Theorem r19.42v 2634

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 2633	. 2 |- ( E. x e. A ( ps /\ ph ) <-> ( E. x e. A ps /\ ph ) )
2		ancom 266	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
3	2	rexbii 2484	. 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 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-rex 2461

This theorem is referenced by:  ceqsrexbv  2870  ceqsrex2v  2871  2reuswapdc  2943  iunrab  3936  iunin2  3952  iundif2ss  3954  iunopab  4283  elxp2  4646  cnvuni  4815  elunirn  5769  f1oiso  5829  oprabrexex2  6133  genpdflem  7508  1idprl  7591  1idpru  7592  ltexprlemm  7601  rexuz2  9583  4fvwrd4  10142  divalgb  11932