Theorem 19.42v 1957

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  exdistr  1958  19.42vv  1961  19.42vvv  1963  4exdistr  1965  2sb5  2271  eeeanv  2346  eu6lem  2567  rexcom4a  3289  cbvrexdva2OLD  3346  ceqsex2  3529  ceqsex2v  3530  reuind  3749  2reu5lem3  3753  sbccomlem  3864  bm1.3ii  5302  eqvinop  5487  dfid2  5576  dmopabss  5918  dmopab3  5919  dmres  6003  ssrnres  6177  mptpreima  6237  resco  6249  mptfnf  6685  brprcneu  6881  brprcneuALT  6882  fndmin  7046  fliftf  7314  dfoprab2  7469  dmoprab  7512  dmoprabss  7513  fnoprabg  7533  uniuni  7751  zfrep6  7943  opabex3d  7954  opabex3rd  7955  opabex3  7956  fsplit  8105  eroveu  8808  rexdif1enOLD  9161  ensymfib  9189  rankuni  9860  aceq1  10114  dfac3  10118  kmlem14  10160  kmlem15  10161  axdc2lem  10445  1idpr  11026  ltexprlem1  11033  ltexprlem4  11036  xpcogend  14925  shftdm  15022  joindm  18332  meetdm  18346  toprntopon  22647  ntreq0  22801  cnextf  23790  dmscut  27537  adjeu  31397  rexunirn  31987  fpwrelmapffslem  32212  mxidlnzrb  32857  tgoldbachgt  33961  bnj1019  34076  bnj1209  34093  bnj1033  34266  bnj1189  34306  satfdm  34646  dfiota3  35187  brimg  35201  funpartlem  35206  bj-eeanvw  35894  bj-snsetex  36147  bj-snglc  36153  bj-bm1.3ii  36248  bj-dfid2ALT  36249  bj-restuni  36281  bj-xpcossxp  36373  bj-imdirco  36374  itg2addnc  36845  sbccom2lem  37295  eldmres  37441  rnxrn  37571  coss1cnvres  37590  nnoeomeqom  42364  rp-isfinite6  42571  undmrnresiss  42657  elintima  42706  pm11.58  43451  pm11.71  43458  2sbc5g  43477  iotasbc2  43481  ax6e2nd  43621  ax6e2ndVD  43971  ax6e2ndALT  43993  stoweidlem60  45075  mofeu  47602  elpglem3  47846