Theorem r19.42v 2623

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 2622	. 2 |- ( E. x e. A ( ps /\ ph ) <-> ( E. x e. A ps /\ ph ) )
2		ancom 264	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
3	2	rexbii 2473	. 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 2445

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-rex 2450

This theorem is referenced by:  ceqsrexbv  2857  ceqsrex2v  2858  2reuswapdc  2930  iunrab  3913  iunin2  3929  iundif2ss  3931  iunopab  4259  elxp2  4622  cnvuni  4790  elunirn  5734  f1oiso  5794  oprabrexex2  6098  genpdflem  7448  1idprl  7531  1idpru  7532  ltexprlemm  7541  rexuz2  9519  4fvwrd4  10075  divalgb  11862