Theorem 19.42v 1918

Description: Version of 19.42 2105 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 1914	. 2 |- ( E. x ( ps /\ ph ) <-> ( E. x ps /\ ph ) )
2		exancom 1787	. 2 |- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
3		ancom 466	. 2 |- ( ( ph /\ E. x ps ) <-> ( E. x ps /\ ph ) )
4	1, 2, 3	3bitr4i 292	1 |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )

Syntax hints:   <-> wb 196   /\ wa 384   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  exdistr  1919  19.42vv  1920  19.42vvv  1921  4exdistr  1924  eeeanv  2183  2sb5  2443  rexcom4a  3226  ceqsex2  3244  reuind  3411  2reu5lem3  3415  sbccomlem  3508  bm1.3ii  4784  eqvinop  4955  dmopabss  5336  dmopab3  5337  mptpreima  5628  mptfnf  6015  brprcneu  6184  fndmin  6324  fliftf  6565  dfoprab2  6701  dmoprab  6741  dmoprabss  6742  fnoprabg  6761  uniuni  6971  zfrep6  7134  opabex3d  7145  opabex3  7146  fsplit  7282  eroveu  7842  rankuni  8726  aceq1  8940  dfac3  8944  kmlem14  8985  kmlem15  8986  axdc2lem  9270  1idpr  9851  ltexprlem1  9858  ltexprlem4  9861  xpcogend  13713  shftdm  13811  joindm  17003  meetdm  17017  toprntopon  20729  ntreq0  20881  cnextf  21870  adjeu  28748  rexunirn  29331  fpwrelmapffslem  29507  tgoldbachgt  30741  bnj1019  30850  bnj1209  30867  bnj1033  31037  bnj1189  31077  dmscut  31918  dfiota3  32030  brimg  32044  funpartlem  32049  bj-eeanvw  32704  bj-rexcom4  32869  bj-rexcom4a  32870  bj-snsetex  32951  bj-snglc  32957  bj-restuni  33050  itg2addnc  33464  sbccom2lem  33929  eldmres  34036  rp-isfinite6  37864  undmrnresiss  37910  elintima  37945  pm11.58  38590  pm11.71  38597  2sbc5g  38617  iotasbc2  38621  ax6e2nd  38774  ax6e2ndVD  39144  ax6e2ndALT  39166  stoweidlem60  40277  elpglem3  42456