Theorem 19.42v 1954

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

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781

This theorem is referenced by:  exdistr  1955  19.42vv  1958  19.42vvv  1960  19.42vvvOLD  1961  4exdistr  1963  2sb5  2282  eeeanv  2371  eu6lem  2658  rexcom4  3249  rexcom4a  3251  cbvrexdva2  3457  ceqsex2  3543  ceqsex2v  3544  reuind  3744  2reu5lem3  3748  sbccomlem  3853  bm1.3ii  5206  eqvinop  5378  dmopabss  5787  dmopab3  5788  dmres  5875  ssrnres  6035  mptpreima  6092  resco  6103  mptfnf  6483  brprcneu  6662  fndmin  6815  fliftf  7068  dfoprab2  7212  dmoprab  7255  dmoprabss  7256  fnoprabg  7275  uniuni  7484  zfrep6  7656  opabex3d  7666  opabex3rd  7667  opabex3  7668  fsplit  7812  fsplitOLD  7813  eroveu  8392  rankuni  9292  aceq1  9543  dfac3  9547  kmlem14  9589  kmlem15  9590  axdc2lem  9870  1idpr  10451  ltexprlem1  10458  ltexprlem4  10461  xpcogend  14334  shftdm  14430  joindm  17613  meetdm  17627  toprntopon  21533  ntreq0  21685  cnextf  22674  adjeu  29666  rexunirn  30256  fpwrelmapffslem  30468  mxidlnzrb  30981  tgoldbachgt  31934  bnj1019  32051  bnj1209  32068  bnj1033  32241  bnj1189  32281  satfdm  32616  dmscut  33272  dfiota3  33384  brimg  33398  funpartlem  33403  bj-eeanvw  34047  bj-snsetex  34278  bj-snglc  34284  bj-bm1.3ii  34360  bj-restuni  34391  itg2addnc  34961  sbccom2lem  35417  eldmres  35545  rnxrn  35661  rp-isfinite6  39933  undmrnresiss  40013  elintima  40047  pm11.58  40771  pm11.71  40778  2sbc5g  40797  iotasbc2  40801  ax6e2nd  40941  ax6e2ndVD  41291  ax6e2ndALT  41313  stoweidlem60  42394  elpglem3  44864