Theorem 19.41v 1951

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  19.41vv  1952  19.41vvv  1953  19.41vvvv  1954  19.42v  1955  exdistrv  1957  r19.41v  3168  gencbvex  3501  euxfrw  3681  euxfr  3683  euind  3684  dfdif3OLD  4072  zfpair  5368  opabn0  5509  eliunxp  5794  relop  5807  dmuni  5871  dminss  6119  imainss  6120  cnvresima  6196  rnco  6218  rncoOLD  6219  coass  6232  xpco  6255  rnoprab  7473  eloprabga  7477  f11o  7901  frxp  8078  omeu  8522  domen  8910  xpassen  9011  enfii  9122  ttrclselem2  9647  kmlem3  10075  cflem  10167  cflemOLD  10168  genpass  10932  ltexprlem4  10962  hasheqf1oi  14286  elwspths2spth  30055  bnj534  34915  bnj906  35105  bnj908  35106  bnj916  35108  bnj983  35126  bnj986  35130  fmla0  35595  fmlasuc0  35597  rexxfr3dALT  35852  dftr6  35964  bj-eeanvw  36955  bj-substw  36965  bj-csbsnlem  37148  bj-clel3gALT  37293  bj-rest10  37338  bj-restuni  37347  bj-imdirco  37442  bj-ccinftydisj  37465  wl-dfclab  37837  eldmqsres2  38542  disjdmqscossss  39154  prter2  39254  dihglb2  41715  prjspeclsp  42967  pm11.6  44745  pm11.71  44750  rfcnnnub  45393  eliunxp2  48691  thinccic  49827