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  2279  eeeanv  2352  eu6lem  2573  r3ex  3184  rexcom4a  3277  cbvrexdva2OLD  3333  ceqsex2  3519  ceqsex2v  3520  reuind  3741  2reu5lem3  3745  sbccomlemOLD  3850  bm1.3iiOLD  5277  eqvinop  5467  dfid2  5555  dmopabss  5903  dmopab3  5904  dmxp  5913  rnopabss  5940  rnopab3  5941  dmres  6004  ssrnres  6172  mptpreima  6232  resco  6244  mptfnf  6678  brprcneu  6871  brprcneuALT  6872  fndmin  7040  fliftf  7313  dfoprab2  7470  dmoprab  7515  dmoprabss  7516  fnoprabg  7535  uniuni  7761  zfrep6  7958  opabex3d  7969  opabex3rd  7970  opabex3  7971  fsplit  8121  eroveu  8831  rexdif1enOLD  9178  ensymfib  9203  rankuni  9882  aceq1  10136  dfac3  10140  kmlem14  10183  kmlem15  10184  axdc2lem  10467  1idpr  11048  ltexprlem1  11055  ltexprlem4  11058  xpcogend  14998  shftdm  15095  joindm  18390  meetdm  18404  toprntopon  22868  ntreq0  23020  cnextf  24009  dmscut  27780  adjeu  31875  rexunirn  32478  fpwrelmapffslem  32714  mxidlnzrb  33500  tgoldbachgt  34700  bnj1019  34815  bnj1209  34832  bnj1033  35005  bnj1189  35045  satfdm  35396  dfiota3  35946  brimg  35960  funpartlem  35965  bj-eeanvw  36736  bj-snsetex  36986  bj-snglc  36992  bj-bm1.3ii  37087  bj-dfid2ALT  37088  bj-restuni  37120  bj-xpcossxp  37212  bj-imdirco  37213  itg2addnc  37703  sbccom2lem  38153  eldmres  38293  rnxrn  38421  coss1cnvres  38440  nnoeomeqom  43311  rp-isfinite6  43517  undmrnresiss  43603  elintima  43652  pm11.58  44389  pm11.71  44396  2sbc5g  44415  iotasbc2  44419  ax6e2nd  44558  ax6e2ndVD  44907  ax6e2ndALT  44929  modelaxreplem3  44980  stoweidlem60  46069  coxp  48791  mofeu  48806  elpglem3  49557