Theorem 19.41v 1954

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

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  19.42v  1958  exdistrv  1960  r19.41v  3273  gencbvex  3478  euxfrw  3651  euxfr  3653  euind  3654  dfdif3  4045  zfpair  5339  opabn0  5459  eliunxp  5735  relop  5748  dmuni  5812  dminss  6045  imainss  6046  cnvresima  6122  rnco  6145  coass  6158  xpco  6181  rnoprab  7356  eloprabga  7360  f11o  7763  frxp  7938  omeu  8378  domen  8706  xpassen  8806  dif1en  8907  enfii  8932  kmlem3  9839  cflem  9933  genpass  10696  ltexprlem4  10726  hasheqf1oi  13994  elwspths2spth  28233  bnj534  32619  bnj906  32810  bnj908  32811  bnj916  32813  bnj983  32831  bnj986  32835  fmla0  33244  fmlasuc0  33246  dftr6  33624  ttrclselem2  33712  bj-eeanvw  34822  bj-substw  34831  bj-csbsnlem  35015  bj-clel3gALT  35148  bj-rest10  35186  bj-restuni  35195  bj-imdirco  35288  bj-ccinftydisj  35311  wl-dfclab  35674  eldmqsres2  36349  prter2  36822  dihglb2  39283  prjspeclsp  40372  pm11.6  41899  pm11.71  41904  rfcnnnub  42468  eliunxp2  45557  thinccic  46230