Theorem 19.42v 1954

Description: Version of 19.42 2236 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 464	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 306	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  exdistr  1955  19.42vv  1958  19.42vvv  1960  19.42vvvOLD  1961  4exdistr  1963  2sb5  2278  eeeanv  2360  eu6lem  2633  rexcom4  3212  rexcom4a  3214  cbvrexdva2  3404  ceqsex2  3491  ceqsex2v  3492  reuind  3692  2reu5lem3  3696  sbccomlem  3799  bm1.3ii  5170  eqvinop  5343  dmopabss  5751  dmopab3  5752  dmres  5840  ssrnres  6002  mptpreima  6059  resco  6070  mptfnf  6455  brprcneu  6637  fndmin  6792  fliftf  7047  dfoprab2  7191  dmoprab  7234  dmoprabss  7235  fnoprabg  7254  uniuni  7464  zfrep6  7638  opabex3d  7648  opabex3rd  7649  opabex3  7650  fsplit  7795  fsplitOLD  7796  eroveu  8375  rankuni  9276  aceq1  9528  dfac3  9532  kmlem14  9574  kmlem15  9575  axdc2lem  9859  1idpr  10440  ltexprlem1  10447  ltexprlem4  10450  xpcogend  14325  shftdm  14422  joindm  17605  meetdm  17619  toprntopon  21530  ntreq0  21682  cnextf  22671  adjeu  29672  rexunirn  30263  fpwrelmapffslem  30494  mxidlnzrb  31052  tgoldbachgt  32044  bnj1019  32161  bnj1209  32178  bnj1033  32351  bnj1189  32391  satfdm  32729  dmscut  33385  dfiota3  33497  brimg  33511  funpartlem  33516  bj-eeanvw  34160  bj-snsetex  34399  bj-snglc  34405  bj-bm1.3ii  34481  bj-restuni  34512  bj-xpcossxp  34604  bj-imdirco  34605  itg2addnc  35111  sbccom2lem  35562  eldmres  35690  rnxrn  35806  rp-isfinite6  40226  undmrnresiss  40304  elintima  40354  pm11.58  41094  pm11.71  41101  2sbc5g  41120  iotasbc2  41124  ax6e2nd  41264  ax6e2ndVD  41614  ax6e2ndALT  41636  stoweidlem60  42702  elpglem3  45242