Theorem 19.42v 1953

Description: Version of 19.42 2237 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 1949	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1861	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 303	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  exdistr  1954  19.42vv  1957  19.42vvv  1959  4exdistr  1961  2sb5  2278  eeeanv  2348  eu6lem  2566  r3ex  3174  rexcom4a  3265  cbvrexdva2OLD  3320  ceqsex2  3498  ceqsex2v  3499  reuind  3721  2reu5lem3  3725  sbccomlemOLD  3830  bm1.3iiOLD  5252  eqvinop  5442  dfid2  5528  dmopabss  5872  dmopab3  5873  dmxp  5882  rnopabss  5908  rnopab3  5909  dmres  5972  ssrnres  6139  mptpreima  6199  resco  6211  mptfnf  6635  brprcneu  6830  brprcneuALT  6831  fndmin  6999  fliftf  7272  dfoprab2  7427  dmoprab  7472  dmoprabss  7473  fnoprabg  7492  uniuni  7718  zfrep6  7913  opabex3d  7923  opabex3rd  7924  opabex3  7925  fsplit  8073  eroveu  8762  rexdif1enOLD  9100  ensymfib  9125  rankuni  9792  aceq1  10046  dfac3  10050  kmlem14  10093  kmlem15  10094  axdc2lem  10377  1idpr  10958  ltexprlem1  10965  ltexprlem4  10968  xpcogend  14916  shftdm  15013  joindm  18314  meetdm  18328  toprntopon  22845  ntreq0  22997  cnextf  23986  dmscut  27757  adjeu  31868  rexunirn  32471  fpwrelmapffslem  32705  mxidlnzrb  33444  tgoldbachgt  34647  bnj1019  34762  bnj1209  34779  bnj1033  34952  bnj1189  34992  satfdm  35349  dfiota3  35904  brimg  35918  funpartlem  35923  bj-eeanvw  36694  bj-snsetex  36944  bj-snglc  36950  bj-bm1.3ii  37045  bj-dfid2ALT  37046  bj-restuni  37078  bj-xpcossxp  37170  bj-imdirco  37171  itg2addnc  37661  sbccom2lem  38111  eldmres  38252  rnxrn  38377  coss1cnvres  38401  nnoeomeqom  43294  rp-isfinite6  43500  undmrnresiss  43586  elintima  43635  pm11.58  44372  pm11.71  44379  2sbc5g  44398  iotasbc2  44402  ax6e2nd  44541  ax6e2ndVD  44890  ax6e2ndALT  44912  modelaxreplem3  44963  stoweidlem60  46051  coxp  48814  mofeu  48829  uobffth  49200  uobeqw  49201  elpglem3  49695