Theorem 19.42v 1958

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

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  exdistr  1959  19.42vv  1962  19.42vvv  1964  4exdistr  1966  2sb5  2275  eeeanv  2350  eu6lem  2573  rexcom4a  3181  cbvrexdva2  3382  ceqsex2  3472  ceqsex2v  3473  reuind  3683  2reu5lem3  3687  sbccomlem  3799  bm1.3ii  5221  eqvinop  5395  dfid2  5482  dmopabss  5816  dmopab3  5817  dmres  5902  ssrnres  6070  mptpreima  6130  resco  6143  mptfnf  6552  brprcneu  6747  fvprc  6748  fndmin  6904  fliftf  7166  dfoprab2  7311  dmoprab  7354  dmoprabss  7355  fnoprabg  7375  uniuni  7590  zfrep6  7771  opabex3d  7781  opabex3rd  7782  opabex3  7783  fsplit  7928  fsplitOLD  7929  eroveu  8559  rexdif1en  8906  ensymfib  8930  rankuni  9552  aceq1  9804  dfac3  9808  kmlem14  9850  kmlem15  9851  axdc2lem  10135  1idpr  10716  ltexprlem1  10723  ltexprlem4  10726  xpcogend  14613  shftdm  14710  joindm  18008  meetdm  18022  toprntopon  21982  ntreq0  22136  cnextf  23125  adjeu  30152  rexunirn  30741  fpwrelmapffslem  30969  mxidlnzrb  31546  tgoldbachgt  32543  bnj1019  32659  bnj1209  32676  bnj1033  32849  bnj1189  32889  satfdm  33231  dmscut  33932  dfiota3  34152  brimg  34166  funpartlem  34171  bj-eeanvw  34822  bj-snsetex  35080  bj-snglc  35086  bj-bm1.3ii  35162  bj-dfid2ALT  35163  bj-restuni  35195  bj-xpcossxp  35287  bj-imdirco  35288  itg2addnc  35758  sbccom2lem  36209  eldmres  36335  rnxrn  36451  rp-isfinite6  41023  undmrnresiss  41101  elintima  41150  pm11.58  41897  pm11.71  41904  2sbc5g  41923  iotasbc2  41927  ax6e2nd  42067  ax6e2ndVD  42417  ax6e2ndALT  42439  stoweidlem60  43491  mofeu  46063  elpglem3  46304