Theorem 19.42v 1950

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776

This theorem is referenced by:  exdistr  1951  19.42vv  1954  19.42vvv  1956  4exdistr  1958  2sb5  2275  eeeanv  2350  eu6lem  2570  r3ex  3195  rexcom4a  3289  cbvrexdva2OLD  3347  ceqsex2  3534  ceqsex2v  3535  reuind  3761  2reu5lem3  3765  sbccomlemOLD  3878  bm1.3iiOLD  5307  eqvinop  5497  dfid2  5584  dmopabss  5931  dmopab3  5932  dmxp  5941  rnopabss  5968  rnopab3  5969  dmres  6031  ssrnres  6199  mptpreima  6259  resco  6271  mptfnf  6703  brprcneu  6896  brprcneuALT  6897  fndmin  7064  fliftf  7334  dfoprab2  7490  dmoprab  7534  dmoprabss  7535  fnoprabg  7555  uniuni  7780  zfrep6  7977  opabex3d  7988  opabex3rd  7989  opabex3  7990  fsplit  8140  eroveu  8850  rexdif1enOLD  9197  ensymfib  9221  rankuni  9900  aceq1  10154  dfac3  10158  kmlem14  10201  kmlem15  10202  axdc2lem  10485  1idpr  11066  ltexprlem1  11073  ltexprlem4  11076  xpcogend  15009  shftdm  15106  joindm  18432  meetdm  18446  toprntopon  22946  ntreq0  23100  cnextf  24089  dmscut  27870  adjeu  31917  rexunirn  32519  fpwrelmapffslem  32749  mxidlnzrb  33487  tgoldbachgt  34656  bnj1019  34771  bnj1209  34788  bnj1033  34961  bnj1189  35001  satfdm  35353  dfiota3  35904  brimg  35918  funpartlem  35923  bj-eeanvw  36695  bj-snsetex  36945  bj-snglc  36951  bj-bm1.3ii  37046  bj-dfid2ALT  37047  bj-restuni  37079  bj-xpcossxp  37171  bj-imdirco  37172  itg2addnc  37660  sbccom2lem  38110  eldmres  38251  rnxrn  38379  coss1cnvres  38398  nnoeomeqom  43301  rp-isfinite6  43507  undmrnresiss  43593  elintima  43642  pm11.58  44385  pm11.71  44392  2sbc5g  44411  iotasbc2  44415  ax6e2nd  44555  ax6e2ndVD  44905  ax6e2ndALT  44927  modelaxreplem3  44944  stoweidlem60  46015  mofeu  48677  elpglem3  48943