Theorem r19.42v 2586

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

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-rex 2420

This theorem is referenced by:  ceqsrexbv  2811  ceqsrex2v  2812  2reuswapdc  2883  iunrab  3855  iunin2  3871  iundif2ss  3873  iunopab  4198  elxp2  4552  cnvuni  4720  elunirn  5660  f1oiso  5720  oprabrexex2  6021  genpdflem  7308  1idprl  7391  1idpru  7392  ltexprlemm  7401  rexuz2  9369  4fvwrd4  9910  divalgb  11611