Theorem 19.42v 1761

Description: Version of 19.42 1958 with a dv condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
19.42v	|- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )

Distinct variable group:   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem 19.42v

Step	Hyp	Ref	Expression
1		19.41v 1757	. 2 |- ( E. x ( ps /\ ph ) <-> ( E. x ps /\ ph ) )
2		exancom 1658	. 2 |- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
3		ancom 450	. 2 |- ( ( ph /\ E. x ps ) <-> ( E. x ps /\ ph ) )
4	1, 2, 3	3bitr4i 277	1 |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )

Syntax hints:   <-> wb 184   /\ wa 369   E.wex 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600

This theorem is referenced by:  exdistr  1762  19.42vv  1763  19.42vvv  1764  4exdistr  1767  eeeanv  1975  cbvex2OLD  2015  2sb5  2173  rexcom4a  3116  ceqsex2  3133  reuind  3289  2reu5lem3  3293  sbccomlem  3392  bm1.3ii  4561  eqvinop  4721  dmopabss  5204  dmopab3  5205  mptpreima  5490  brprcneu  5849  fndmin  5979  fliftf  6198  dfoprab2  6328  dmoprab  6368  dmoprabss  6369  fnoprabg  6388  uniuni  6594  zfrep6  6753  opabex3d  6763  opabex3  6764  fsplit  6890  eroveu  7408  rankuni  8284  aceq1  8501  dfac3  8505  kmlem14  8546  kmlem15  8547  axdc2lem  8831  1idpr  9410  ltexprlem1  9417  ltexprlem4  9420  shftdm  12885  joindm  15611  meetdm  15625  ntreq0  19555  cnextf  20543  usg2spot2nb  25041  adjeu  26784  rexunirn  27366  mptfnf  27475  fpwrelmapffslem  27531  dfiota3  29548  brimg  29562  funpartlem  29567  itg2addnc  30044  sbccom2lem  30504  pm11.58  31250  pm11.71  31257  2sbc5g  31277  iotasbc2  31281  stoweidlem60  31731  ax6e2nd  33064  ax6e2ndVD  33441  ax6e2ndALT  33463  bnj1019  33571  bnj1209  33588  bnj1033  33758  bnj1189  33798  bj-eeanvw  34015  bj-rexcom4  34193  bj-rexcom4a  34194  bj-snsetex  34269  bj-snglc  34275  rp-isfinite6  37447  xpcogend  37466