Theorem 19.41v 1949

Description: Version of 19.41 2236 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1967. (Revised by Rohan Ridenour, 15-Apr-2022.)

Assertion

Ref	Expression
19.41v	⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.41v

Step	Hyp	Ref	Expression
1		19.40 1886	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1912	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 617	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 471	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1917	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 407	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 209	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:  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  19.42v  1953  exdistrv  1955  r19.41v  3159  gencbvex  3498  euxfrw  3683  euxfr  3685  euind  3686  dfdif3OLD  4071  zfpair  5363  opabn0  5500  eliunxp  5784  relop  5797  dmuni  5861  dminss  6106  imainss  6107  cnvresima  6183  rnco  6205  coass  6218  xpco  6241  rnoprab  7458  eloprabga  7462  f11o  7889  frxp  8066  omeu  8510  domen  8894  xpassen  8995  dif1enOLD  9086  enfii  9110  ttrclselem2  9641  kmlem3  10066  cflem  10158  cflemOLD  10159  genpass  10922  ltexprlem4  10952  hasheqf1oi  14276  elwspths2spth  29930  bnj534  34708  bnj906  34899  bnj908  34900  bnj916  34902  bnj983  34920  bnj986  34924  fmla0  35357  fmlasuc0  35359  rexxfr3dALT  35614  dftr6  35726  bj-eeanvw  36689  bj-substw  36698  bj-csbsnlem  36879  bj-clel3gALT  37024  bj-rest10  37064  bj-restuni  37073  bj-imdirco  37166  bj-ccinftydisj  37189  wl-dfclab  37572  eldmqsres2  38264  disjdmqscossss  38783  prter2  38862  dihglb2  41324  prjspeclsp  42588  pm11.6  44368  pm11.71  44373  rfcnnnub  45017  eliunxp2  48322  thinccic  49460