Theorem 19.41v 1950

Description: Version of 19.41 2238 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1968. (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 1887	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1913	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 617	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 471	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1918	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 407	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 209	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃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 207  df-an 396  df-ex 1781

This theorem is referenced by:  19.41vv  1951  19.41vvv  1952  19.41vvvv  1953  19.42v  1954  exdistrv  1956  r19.41v  3162  gencbvex  3496  euxfrw  3680  euxfr  3682  euind  3683  dfdif3OLD  4068  zfpair  5359  opabn0  5493  eliunxp  5777  relop  5790  dmuni  5854  dminss  6100  imainss  6101  cnvresima  6177  rnco  6199  rncoOLD  6200  coass  6213  xpco  6236  rnoprab  7451  eloprabga  7455  f11o  7879  frxp  8056  omeu  8500  domen  8884  xpassen  8984  enfii  9095  ttrclselem2  9616  kmlem3  10044  cflem  10136  cflemOLD  10137  genpass  10900  ltexprlem4  10930  hasheqf1oi  14258  elwspths2spth  29946  bnj534  34749  bnj906  34940  bnj908  34941  bnj916  34943  bnj983  34961  bnj986  34965  fmla0  35424  fmlasuc0  35426  rexxfr3dALT  35681  dftr6  35793  bj-eeanvw  36753  bj-substw  36762  bj-csbsnlem  36943  bj-clel3gALT  37088  bj-rest10  37128  bj-restuni  37137  bj-imdirco  37230  bj-ccinftydisj  37253  wl-dfclab  37636  eldmqsres2  38328  disjdmqscossss  38847  prter2  38926  dihglb2  41387  prjspeclsp  42651  pm11.6  44431  pm11.71  44436  rfcnnnub  45079  eliunxp2  48371  thinccic  49509