Theorem r19.42v 2614

Description: Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)

Assertion

Ref	Expression
r19.42v	|- ( E. x e. A ( ph /\ ps ) <-> ( ph /\ E. x e. A ps ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem r19.42v

Step	Hyp	Ref	Expression
1		r19.41v 2613	. 2 |- ( E. x e. A ( ps /\ ph ) <-> ( E. x e. A ps /\ ph ) )
2		ancom 264	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
3	2	rexbii 2464	. 2 |- ( E. x e. A ( ph /\ ps ) <-> E. x e. A ( ps /\ ph ) )
4		ancom 264	. 2 |- ( ( ph /\ E. x e. A ps ) <-> ( E. x e. A ps /\ ph ) )
5	1, 3, 4	3bitr4i 211	1 |- ( E. x e. A ( ph /\ ps ) <-> ( ph /\ E. x e. A ps ) )

Syntax hints:   /\ wa 103   <-> wb 104   E.wrex 2436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-rex 2441

This theorem is referenced by:  ceqsrexbv  2843  ceqsrex2v  2844  2reuswapdc  2916  iunrab  3896  iunin2  3912  iundif2ss  3914  iunopab  4241  elxp2  4604  cnvuni  4772  elunirn  5716  f1oiso  5776  oprabrexex2  6078  genpdflem  7427  1idprl  7510  1idpru  7511  ltexprlemm  7520  rexuz2  9492  4fvwrd4  10039  divalgb  11815