Theorem rcla4ev 1403

Description: Restricted existential specialization with implicit substitution.

Hypothesis

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

Assertion

Ref	Expression
rcla4ev	|- ((A e. B /\ ps) -> E.x e. B ph)

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

Proof of Theorem rcla4ev

Step	Hyp	Ref	Expression
1		eleq1 1149	. . . . 5 |- (x = A -> (x e. B <-> A e. B))
2		rcla4v.1	. . . . 5 |- (x = A -> (ph <-> ps))
3	1, 2	anbi12d 476	. . . 4 |- (x = A -> ((x e. B /\ ph) <-> (A e. B /\ ps)))
4	3	cla4egv 1397	. . 3 |- (A e. B -> ((A e. B /\ ps) -> E.x(x e. B /\ ph)))
5	4	anabsi5 377	. 2 |- ((A e. B /\ ps) -> E.x(x e. B /\ ph))
6		df-rex 1206	. 2 |- (E.x e. B ph <-> E.x(x e. B /\ ph))
7	5, 6	sylibr 175	1 |- ((A e. B /\ ps) -> E.x e. B ph)

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  E.wex 678   = wceq 1091   e. wcel 1092  E.wrex 1202

This theorem is referenced by:  rcla42ev 1405  supsn 2168  wefrc 2195  onfr 2237  ordunidif 2260  onssmin 2263  onuninsuc 2356  tfrlem12 2960  oawordeulem 3156  oaass 3163  oen0 3165  snfi 3337  mapenlem2 3385  onfin 3415  pssnn 3428  ssnn 3429  unfi 3441  trcl 3489  r1ord 3499  tz9.12lem3 3505  tz9.12 3506  scottex 3541  scott0 3542  aceq6b 3565  numth2 3600  oncardval 3626  cardaleph 3690  cardalephex 3691  cflem 3700  cflecard 3707  cfsuc 3709  posex 4422  nn2get 4438  nndiv 4453  nominpos 4509  uzwo 4605  nnwoOLD 4608  btwnz 4613  zqt 4632  qbtwnre 4650  sqrlem6 4736  clim0 4882  ruclem33 4917  infxpidmlem11 4943  hlim0 5140  projlem8 5200  projlem10 5202  ococint 5298  spanvalt 5300  spanclt 5305  shsumval2 5361  h1de2ctlem 5460  spansncol 5473  pjoml5 5498  strlem1 5691  str 5698  cvcon3t 5716  cvnbtwnt 5718  shatomic 5753  atcvat4 5775  mdsymlem2 5777

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-rex 1206  df-v 1349

metamath.org