Theorem 19.42v 1826

Description: Version of 19.42 2029 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 1822	. 2 |- ( E. x ( ps /\ ph ) <-> ( E. x ps /\ ph ) )
2		exancom 1718	. 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 1659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797

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

This theorem is referenced by:  exdistr  1827  19.42vv  1828  19.42vvv  1829  4exdistr  1832  eeeanv  2046  2sb5  2239  rexcom4a  3108  ceqsex2  3125  reuind  3281  2reu5lem3  3285  sbccomlem  3376  bm1.3ii  4551  eqvinop  4706  dmopabss  5066  dmopab3  5067  mptpreima  5348  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  7466  rankuni  8333  aceq1  8546  dfac3  8550  kmlem14  8591  kmlem15  8592  axdc2lem  8876  1idpr  9453  ltexprlem1  9460  ltexprlem4  9463  xpcogend  13017  shftdm  13113  joindm  16191  meetdm  16205  ntreq0  20015  cnextf  21003  usg2spot2nb  25629  adjeu  27368  rexunirn  27953  fpwrelmapffslem  28151  bnj1019  29370  bnj1209  29387  bnj1033  29557  bnj1189  29597  dfiota3  30466  brimg  30480  funpartlem  30485  bj-eeanvw  31038  bj-rexcom4  31220  bj-rexcom4a  31221  bj-snsetex  31297  bj-snglc  31303  itg2addnc  31690  sbccom2lem  32058  rp-isfinite6  35852  elintima  35874  pm11.58  36367  pm11.71  36374  2sbc5g  36394  iotasbc2  36398  ax6e2nd  36552  ax6e2ndVD  36935  ax6e2ndALT  36957  stoweidlem60  37480