Theorem 19.42v 1827

Description: Version of 19.42 2031 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 1823	. 2 |- ( E. x ( ps /\ ph ) <-> ( E. x ps /\ ph ) )
2		exancom 1716	. 2 |- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
3		ancom 451	. 2 |- ( ( ph /\ E. x ps ) <-> ( E. x ps /\ ph ) )
4	1, 2, 3	3bitr4i 280	1 |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )

Syntax hints:   <-> wb 187   /\ wa 370   E.wex 1657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658

This theorem is referenced by:  exdistr  1828  19.42vv  1829  19.42vvv  1830  4exdistr  1833  eeeanv  2048  2sb5  2242  rexcom4a  3102  ceqsex2  3119  reuind  3275  2reu5lem3  3279  sbccomlem  3370  bm1.3ii  4549  eqvinop  4705  dmopabss  5065  dmopab3  5066  mptpreima  5347  mptfnf  5717  brprcneu  5874  fndmin  6004  fliftf  6223  dfoprab2  6351  dmoprab  6391  dmoprabss  6392  fnoprabg  6411  uniuni  6614  zfrep6  6775  opabex3d  6785  opabex3  6786  fsplit  6912  eroveu  7469  rankuni  8342  aceq1  8555  dfac3  8559  kmlem14  8600  kmlem15  8601  axdc2lem  8885  1idpr  9461  ltexprlem1  9468  ltexprlem4  9471  xpcogend  13038  shftdm  13134  joindm  16248  meetdm  16262  ntreq0  20091  cnextf  21079  usg2spot2nb  25791  adjeu  27540  rexunirn  28125  fpwrelmapffslem  28323  bnj1019  29599  bnj1209  29616  bnj1033  29786  bnj1189  29826  dfiota3  30695  brimg  30709  funpartlem  30714  bj-eeanvw  31267  bj-rexcom4  31448  bj-rexcom4a  31449  bj-snsetex  31525  bj-snglc  31531  itg2addnc  31960  sbccom2lem  32328  rp-isfinite6  36133  undmrnresiss  36180  elintima  36215  pm11.58  36710  pm11.71  36717  2sbc5g  36737  iotasbc2  36741  ax6e2nd  36895  ax6e2ndVD  37278  ax6e2ndALT  37300  stoweidlem60  37861