Theorem 19.42v 1954

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

Assertion

Ref	Expression
19.42v	⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.42v

Step	Hyp	Ref	Expression
1		19.41v 1950	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1862	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 303	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  exdistr  1955  19.42vv  1958  19.42vvv  1960  4exdistr  1962  2sb5  2280  eeeanv  2350  eu6lem  2568  r3ex  3171  rexcom4a  3262  ceqsex2  3489  ceqsex2v  3490  reuind  3707  2reu5lem3  3711  sbccomlemOLD  3816  bm1.3iiOLD  5238  eqvinop  5425  dfid2  5511  dmopabss  5857  dmopab3  5858  dmxp  5868  rnopabss  5894  rnopab3  5895  dmres  5960  ssrnres  6125  mptpreima  6185  resco  6197  mptfnf  6616  brprcneu  6812  brprcneuALT  6813  fndmin  6978  fliftf  7249  dfoprab2  7404  dmoprab  7449  dmoprabss  7450  fnoprabg  7469  uniuni  7695  zfrep6  7887  opabex3d  7897  opabex3rd  7898  opabex3  7899  fsplit  8047  eroveu  8736  ensymfib  9093  rankuni  9756  aceq1  10008  dfac3  10012  kmlem14  10055  kmlem15  10056  axdc2lem  10339  1idpr  10920  ltexprlem1  10927  ltexprlem4  10930  xpcogend  14881  shftdm  14978  joindm  18279  meetdm  18293  toprntopon  22840  ntreq0  22992  cnextf  23981  dmscut  27752  adjeu  31869  rexunirn  32471  fpwrelmapffslem  32715  mxidlnzrb  33445  tgoldbachgt  34676  bnj1019  34791  bnj1209  34808  bnj1033  34981  bnj1189  35021  satfdm  35413  dfiota3  35965  brimg  35979  funpartlem  35986  bj-eeanvw  36757  bj-snsetex  37007  bj-snglc  37013  bj-bm1.3ii  37108  bj-dfid2ALT  37109  bj-restuni  37141  bj-xpcossxp  37233  bj-imdirco  37234  itg2addnc  37724  sbccom2lem  38174  eldmres  38319  rnxrn  38455  coss1cnvres  38529  nnoeomeqom  43415  rp-isfinite6  43621  undmrnresiss  43707  elintima  43756  pm11.58  44493  pm11.71  44500  2sbc5g  44519  iotasbc2  44523  ax6e2nd  44661  ax6e2ndVD  45010  ax6e2ndALT  45032  modelaxreplem3  45083  stoweidlem60  46168  coxp  48943  mofeu  48958  uobffth  49329  uobeqw  49330  elpglem3  49824