Theorem 19.42v 1783

Description: Version of 19.42 1980 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 1779	. 2 |- ( E. x ( ps /\ ph ) <-> ( E. x ps /\ ph ) )
2		exancom 1679	. 2 |- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
3		ancom 448	. 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 367   E.wex 1620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621

This theorem is referenced by:  exdistr  1784  19.42vv  1785  19.42vvv  1786  4exdistr  1789  eeeanv  1997  2sb5  2191  rexcom4a  3055  ceqsex2  3072  reuind  3228  2reu5lem3  3232  sbccomlem  3323  bm1.3ii  4491  eqvinop  4646  dmopabss  5127  dmopab3  5128  mptpreima  5408  brprcneu  5767  fndmin  5896  fliftf  6114  dfoprab2  6242  dmoprab  6282  dmoprabss  6283  fnoprabg  6302  uniuni  6508  zfrep6  6667  opabex3d  6677  opabex3  6678  fsplit  6804  eroveu  7324  rankuni  8194  aceq1  8411  dfac3  8415  kmlem14  8456  kmlem15  8457  axdc2lem  8741  1idpr  9318  ltexprlem1  9325  ltexprlem4  9328  xpcogend  12812  shftdm  12906  joindm  15750  meetdm  15764  ntreq0  19664  cnextf  20651  usg2spot2nb  25186  adjeu  26924  rexunirn  27507  mptfnf  27640  fpwrelmapffslem  27705  dfiota3  29726  brimg  29740  funpartlem  29745  itg2addnc  30235  sbccom2lem  30695  pm11.58  31464  pm11.71  31471  2sbc5g  31491  iotasbc2  31495  stoweidlem60  32008  ax6e2nd  33671  ax6e2ndVD  34055  ax6e2ndALT  34077  bnj1019  34185  bnj1209  34202  bnj1033  34372  bnj1189  34412  bj-eeanvw  34614  bj-rexcom4  34792  bj-rexcom4a  34793  bj-snsetex  34869  bj-snglc  34875  rp-isfinite6  38173  elintima  38195