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 1860	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 303	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  exdistr  1954  19.42vv  1957  19.42vvv  1959  4exdistr  1961  2sb5  2281  eeeanv  2356  eu6lem  2576  r3ex  3204  rexcom4a  3298  cbvrexdva2OLD  3358  ceqsex2  3547  ceqsex2v  3548  reuind  3775  2reu5lem3  3779  sbccomlemOLD  3892  bm1.3ii  5320  eqvinop  5507  dfid2  5595  dmopabss  5943  dmopab3  5944  dmxp  5953  dmres  6041  ssrnres  6209  mptpreima  6269  resco  6281  mptfnf  6715  brprcneu  6910  brprcneuALT  6911  fndmin  7078  fliftf  7351  dfoprab2  7508  dmoprab  7552  dmoprabss  7553  fnoprabg  7573  uniuni  7797  zfrep6  7995  opabex3d  8006  opabex3rd  8007  opabex3  8008  fsplit  8158  eroveu  8870  rexdif1enOLD  9225  ensymfib  9250  rankuni  9932  aceq1  10186  dfac3  10190  kmlem14  10233  kmlem15  10234  axdc2lem  10517  1idpr  11098  ltexprlem1  11105  ltexprlem4  11108  xpcogend  15023  shftdm  15120  joindm  18445  meetdm  18459  toprntopon  22952  ntreq0  23106  cnextf  24095  dmscut  27874  adjeu  31921  rexunirn  32520  fpwrelmapffslem  32746  mxidlnzrb  33473  tgoldbachgt  34640  bnj1019  34755  bnj1209  34772  bnj1033  34945  bnj1189  34985  satfdm  35337  dfiota3  35887  brimg  35901  funpartlem  35906  bj-eeanvw  36679  bj-snsetex  36929  bj-snglc  36935  bj-bm1.3ii  37030  bj-dfid2ALT  37031  bj-restuni  37063  bj-xpcossxp  37155  bj-imdirco  37156  itg2addnc  37634  sbccom2lem  38084  eldmres  38226  rnxrn  38354  coss1cnvres  38373  nnoeomeqom  43274  rp-isfinite6  43480  undmrnresiss  43566  elintima  43615  pm11.58  44359  pm11.71  44366  2sbc5g  44385  iotasbc2  44389  ax6e2nd  44529  ax6e2ndVD  44879  ax6e2ndALT  44901  stoweidlem60  45981  mofeu  48561  elpglem3  48805