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  3496  euxfrw  3681  euxfr  3683  euind  3684  dfdif3OLD  4069  zfpair  5360  opabn0  5496  eliunxp  5780  relop  5793  dmuni  5857  dminss  6102  imainss  6103  cnvresima  6179  rnco  6201  coass  6214  xpco  6237  rnoprab  7454  eloprabga  7458  f11o  7882  frxp  8059  omeu  8503  domen  8887  xpassen  8988  enfii  9100  ttrclselem2  9622  kmlem3  10047  cflem  10139  cflemOLD  10140  genpass  10903  ltexprlem4  10933  hasheqf1oi  14258  elwspths2spth  29916  bnj534  34722  bnj906  34913  bnj908  34914  bnj916  34916  bnj983  34934  bnj986  34938  fmla0  35375  fmlasuc0  35377  rexxfr3dALT  35632  dftr6  35744  bj-eeanvw  36707  bj-substw  36716  bj-csbsnlem  36897  bj-clel3gALT  37042  bj-rest10  37082  bj-restuni  37091  bj-imdirco  37184  bj-ccinftydisj  37207  wl-dfclab  37590  eldmqsres2  38282  disjdmqscossss  38801  prter2  38880  dihglb2  41341  prjspeclsp  42605  pm11.6  44385  pm11.71  44390  rfcnnnub  45034  eliunxp2  48338  thinccic  49476