Theorem r19.42v 2654

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 2653	. 2 |- ( E. x e. A ( ps /\ ph ) <-> ( E. x e. A ps /\ ph ) )
2		ancom 266	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
3	2	rexbii 2504	. 2 |- ( E. x e. A ( ph /\ ps ) <-> E. x e. A ( ps /\ ph ) )
4		ancom 266	. 2 |- ( ( ph /\ E. x e. A ps ) <-> ( E. x e. A ps /\ ph ) )
5	1, 3, 4	3bitr4i 212	1 |- ( E. x e. A ( ph /\ ps ) <-> ( ph /\ E. x e. A ps ) )

Syntax hints:   /\ wa 104   <-> wb 105   E.wrex 2476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-rex 2481

This theorem is referenced by:  ceqsrexbv  2895  ceqsrex2v  2896  2reuswapdc  2968  iunrab  3964  iunin2  3980  iundif2ss  3982  iunopab  4316  elxp2  4681  cnvuni  4852  elunirn  5813  f1oiso  5873  oprabrexex2  6187  genpdflem  7574  1idprl  7657  1idpru  7658  ltexprlemm  7667  rexuz2  9655  4fvwrd4  10215  divalgb  12090