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 1885	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1911	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 616	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 471	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1916	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 407	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 209	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  19.42v  1953  exdistrv  1955  r19.41v  3195  gencbvex  3553  euxfrw  3743  euxfr  3745  euind  3746  dfdif3OLD  4141  zfpair  5439  opabn0  5572  eliunxp  5862  relop  5875  dmuni  5939  dminss  6184  imainss  6185  cnvresima  6261  rnco  6283  coass  6296  xpco  6320  rnoprab  7554  eloprabga  7558  f11o  7987  frxp  8167  omeu  8641  domen  9021  xpassen  9132  dif1enOLD  9228  enfii  9252  ttrclselem2  9795  kmlem3  10222  cflem  10314  cflemOLD  10315  genpass  11078  ltexprlem4  11108  hasheqf1oi  14400  elwspths2spth  30000  bnj534  34715  bnj906  34906  bnj908  34907  bnj916  34909  bnj983  34927  bnj986  34931  fmla0  35350  fmlasuc0  35352  rexxfr3dALT  35607  dftr6  35713  bj-eeanvw  36679  bj-substw  36688  bj-csbsnlem  36869  bj-clel3gALT  37014  bj-rest10  37054  bj-restuni  37063  bj-imdirco  37156  bj-ccinftydisj  37179  wl-dfclab  37550  eldmqsres2  38244  disjdmqscossss  38759  prter2  38837  dihglb2  41299  prjspeclsp  42567  pm11.6  44361  pm11.71  44366  rfcnnnub  44936  eliunxp2  48058  thinccic  48728