Theorem 19.42v 1953

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  exdistr  1954  19.42vv  1957  19.42vvv  1959  4exdistr  1961  2sb5  2278  eeeanv  2348  eu6lem  2566  r3ex  3176  rexcom4a  3267  cbvrexdva2OLD  3323  ceqsex2  3501  ceqsex2v  3502  reuind  3724  2reu5lem3  3728  sbccomlemOLD  3833  bm1.3iiOLD  5257  eqvinop  5447  dfid2  5535  dmopabss  5882  dmopab3  5883  dmxp  5892  rnopabss  5919  rnopab3  5920  dmres  5983  ssrnres  6151  mptpreima  6211  resco  6223  mptfnf  6653  brprcneu  6848  brprcneuALT  6849  fndmin  7017  fliftf  7290  dfoprab2  7447  dmoprab  7492  dmoprabss  7493  fnoprabg  7512  uniuni  7738  zfrep6  7933  opabex3d  7944  opabex3rd  7945  opabex3  7946  fsplit  8096  eroveu  8785  rexdif1enOLD  9123  ensymfib  9148  rankuni  9816  aceq1  10070  dfac3  10074  kmlem14  10117  kmlem15  10118  axdc2lem  10401  1idpr  10982  ltexprlem1  10989  ltexprlem4  10992  xpcogend  14940  shftdm  15037  joindm  18334  meetdm  18348  toprntopon  22812  ntreq0  22964  cnextf  23953  dmscut  27723  adjeu  31818  rexunirn  32421  fpwrelmapffslem  32655  mxidlnzrb  33451  tgoldbachgt  34654  bnj1019  34769  bnj1209  34786  bnj1033  34959  bnj1189  34999  satfdm  35356  dfiota3  35911  brimg  35925  funpartlem  35930  bj-eeanvw  36701  bj-snsetex  36951  bj-snglc  36957  bj-bm1.3ii  37052  bj-dfid2ALT  37053  bj-restuni  37085  bj-xpcossxp  37177  bj-imdirco  37178  itg2addnc  37668  sbccom2lem  38118  eldmres  38259  rnxrn  38384  coss1cnvres  38408  nnoeomeqom  43301  rp-isfinite6  43507  undmrnresiss  43593  elintima  43642  pm11.58  44379  pm11.71  44386  2sbc5g  44405  iotasbc2  44409  ax6e2nd  44548  ax6e2ndVD  44897  ax6e2ndALT  44919  modelaxreplem3  44970  stoweidlem60  46058  coxp  48821  mofeu  48836  uobffth  49207  uobeqw  49208  elpglem3  49702