Theorem 19.42v 1955

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃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 1912

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

This theorem is referenced by:  exdistr  1956  19.42vv  1959  19.42vvv  1961  4exdistr  1963  2sb5  2285  eeeanv  2354  eu6lem  2573  r3ex  3176  rexcom4a  3267  ceqsex2  3481  ceqsex2v  3482  reuind  3699  2reu5lem3  3703  sbccomlemOLD  3808  bm1.3iiOLD  5237  eqvinop  5440  copsexgw  5443  dfid2  5528  dmopabss  5873  dmopab3  5874  dmxp  5884  rnopabss  5910  rnopab3  5911  dmres  5977  ssrnres  6142  mptpreima  6202  resco  6214  mptfnf  6633  brprcneu  6830  brprcneuALT  6831  fndmin  6997  fliftf  7270  dfoprab2  7425  dmoprab  7470  dmoprabss  7471  fnoprabg  7490  uniuni  7716  zfrep6OLD  7908  opabex3d  7918  opabex3rd  7919  opabex3  7920  fsplit  8067  eroveu  8759  ensymfib  9118  rankuni  9787  aceq1  10039  dfac3  10043  kmlem14  10086  kmlem15  10087  axdc2lem  10370  1idpr  10952  ltexprlem1  10959  ltexprlem4  10962  xpcogend  14936  shftdm  15033  joindm  18339  meetdm  18353  toprntopon  22890  ntreq0  23042  cnextf  24031  dmcuts  27783  adjeu  31960  rexunirn  32561  fpwrelmapffslem  32805  mxidlnzrb  33540  tgoldbachgt  34807  bnj1019  34922  bnj1209  34938  bnj1033  35111  bnj1189  35151  satfdm  35551  dfiota3  36103  brimg  36117  funpartlem  36124  bj-eeanvw  37012  bj-snsetex  37270  bj-snglc  37276  bj-bm1.3ii  37371  bj-dfid2ALT  37372  bj-axreprepsep  37382  bj-restuni  37409  bj-xpcossxp  37503  bj-imdirco  37504  itg2addnc  37995  sbccom2lem  38445  eldmres  38598  rnxrn  38742  coss1cnvres  38828  nnoeomeqom  43740  rp-isfinite6  43945  undmrnresiss  44031  elintima  44080  pm11.58  44817  pm11.71  44824  2sbc5g  44843  iotasbc2  44847  ax6e2nd  44985  ax6e2ndVD  45334  ax6e2ndALT  45356  modelaxreplem3  45407  stoweidlem60  46488  coxp  49308  mofeu  49323  uobffth  49693  uobeqw  49694  elpglem3  50188