Theorem rcla4v 1402

Description: Restricted specialization with implicit substitution.

Hypothesis

Ref	Expression
rcla4v.1	|- (x = A -> (ph <-> ps))

Assertion

Ref	Expression
rcla4v	|- (A.x e. B ph -> (A e. B -> ps))

Distinct variable group(s):   x,A   x,B   ps,x

Proof of Theorem rcla4v

Step	Hyp	Ref	Expression
1		df-ral 1205	. 2 |- (A.x e. B ph <-> A.x(x e. B -> ph))
2		eleq1 1149	. . . . 5 |- (x = A -> (x e. B <-> A e. B))
3		rcla4v.1	. . . . 5 |- (x = A -> (ph <-> ps))
4	2, 3	imbi12d 474	. . . 4 |- (x = A -> ((x e. B -> ph) <-> (A e. B -> ps)))
5	4	cla4gv 1396	. . 3 |- (A e. B -> (A.x(x e. B -> ph) -> (A e. B -> ps)))
6	5	pm2.43b 61	. 2 |- (A.x(x e. B -> ph) -> (A e. B -> ps))
7	1, 6	sylbi 174	1 |- (A.x e. B ph -> (A e. B -> ps))

Syntax hints:   -> wi 2   <-> wb 127  A.wal 672   = wceq 1091   e. wcel 1092  A.wral 1201

This theorem is referenced by:  rcla42v 1404  intmin 1982  supmo 2156  supub 2160  suplub 2161  wereu 2197  tfinds 2401  ralxp 2456  funcnvuni 2706  fconstfv 2903  tfrlem2 2950  tz7.49 2997  abianfp 3000  omsmolem 3195  nneneq 3408  unblem1 3431  unblem2 3432  unbnn2 3436  eirrv 3449  dfom3 3477  rankun 3535  aceq3lem 3555  aceq5lem5 3562  aceq5 3563  aceq6b 3565  ac6lem 3575  numthlem 3598  zornlem2 3604  zornlem6 3608  carduni 3664  alephle 3689  cflim 3704  nnleltp1t 4448  uzwo2 4606  uzwo3lem2 4615  zmax 4618  zbtwnre 4619  sqr2irrlem3 4779  infxpidmlem10 4942  hial0 5058  hial2eqt 5060  hlimunii 5143  chcompl 5150  ocorth 5172  ocin 5177  occllem5 5184  occllem6 5185  projlem22 5214  projlem26 5218  pjthlem12 5236  h1de2 5458  pjjs 5585  stge0t 5673  stle1t 5674  mdi 5727  mdbr3 5729  mdbr4 5730  dmdbr 5731  dmdi 5732  atss 5744  atom1d 5750

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-v 1349

metamath.org