Theorem 19.41v 1958

Description: Version of 19.41 2235 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1976. (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 1894	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1920	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 620	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 475	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1925	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 411	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 212	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788

This theorem is referenced by:  19.41vv  1959  19.41vvv  1960  19.41vvvv  1961  19.42v  1962  exdistrv  1964  equsexvwOLD  2015  r19.41v  3250  gencbvex  3454  euxfrw  3623  euxfr  3625  euind  3626  dfdif3  4015  zfpair  5299  opabn0  5419  eliunxp  5691  relop  5704  dmuni  5768  dminss  5996  imainss  5997  cnvresima  6073  rnco  6096  coass  6109  xpco  6132  rnoprab  7292  eloprabga  7296  f11o  7698  frxp  7871  omeu  8291  domen  8619  xpassen  8717  dif1en  8818  enfii  8841  kmlem3  9731  cflem  9825  genpass  10588  ltexprlem4  10618  hasheqf1oi  13883  elwspths2spth  28005  bnj534  32385  bnj906  32577  bnj908  32578  bnj916  32580  bnj983  32598  bnj986  32602  fmla0  33011  fmlasuc0  33013  dftr6  33387  bj-eeanvw  34581  bj-substw  34590  bj-csbsnlem  34775  bj-clel3gALT  34907  bj-rest10  34943  bj-restuni  34952  bj-imdirco  35045  bj-ccinftydisj  35068  wl-dfclab  35433  eldmqsres2  36108  prter2  36581  dihglb2  39042  prjspeclsp  40100  pm11.6  41624  pm11.71  41629  rfcnnnub  42193  eliunxp2  45285  thinccic  45958