Theorem 19.42v 1954

Description: Version of 19.42 2243 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  2284  eeeanv  2354  eu6lem  2573  r3ex  3175  rexcom4a  3266  ceqsex2  3493  ceqsex2v  3494  reuind  3711  2reu5lem3  3715  sbccomlemOLD  3820  bm1.3iiOLD  5247  eqvinop  5435  dfid2  5521  dmopabss  5867  dmopab3  5868  dmxp  5878  rnopabss  5904  rnopab3  5905  dmres  5971  ssrnres  6136  mptpreima  6196  resco  6208  mptfnf  6627  brprcneu  6824  brprcneuALT  6825  fndmin  6990  fliftf  7261  dfoprab2  7416  dmoprab  7461  dmoprabss  7462  fnoprabg  7481  uniuni  7707  zfrep6  7899  opabex3d  7909  opabex3rd  7910  opabex3  7911  fsplit  8059  eroveu  8749  ensymfib  9108  rankuni  9775  aceq1  10027  dfac3  10031  kmlem14  10074  kmlem15  10075  axdc2lem  10358  1idpr  10940  ltexprlem1  10947  ltexprlem4  10950  xpcogend  14897  shftdm  14994  joindm  18296  meetdm  18310  toprntopon  22869  ntreq0  23021  cnextf  24010  dmcuts  27787  adjeu  31964  rexunirn  32566  fpwrelmapffslem  32811  mxidlnzrb  33561  tgoldbachgt  34820  bnj1019  34935  bnj1209  34952  bnj1033  35125  bnj1189  35165  satfdm  35563  dfiota3  36115  brimg  36129  funpartlem  36136  bj-eeanvw  36914  bj-snsetex  37164  bj-snglc  37170  bj-bm1.3ii  37265  bj-dfid2ALT  37266  bj-restuni  37302  bj-xpcossxp  37394  bj-imdirco  37395  itg2addnc  37875  sbccom2lem  38325  eldmres  38472  rnxrn  38616  coss1cnvres  38690  nnoeomeqom  43564  rp-isfinite6  43769  undmrnresiss  43855  elintima  43904  pm11.58  44641  pm11.71  44648  2sbc5g  44667  iotasbc2  44671  ax6e2nd  44809  ax6e2ndVD  45158  ax6e2ndALT  45180  modelaxreplem3  45231  stoweidlem60  46314  coxp  49088  mofeu  49103  uobffth  49473  uobeqw  49474  elpglem3  49968