Theorem 19.41v 1946

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  19.41vv  1947  19.41vvv  1948  19.41vvvv  1949  19.42v  1950  exdistrv  1952  r19.41v  3186  gencbvex  3540  euxfrw  3729  euxfr  3731  euind  3732  dfdif3OLD  4127  zfpair  5426  opabn0  5562  eliunxp  5850  relop  5863  dmuni  5927  dminss  6174  imainss  6175  cnvresima  6251  rnco  6273  coass  6286  xpco  6310  rnoprab  7536  eloprabga  7540  f11o  7969  frxp  8149  omeu  8621  domen  9000  xpassen  9104  dif1enOLD  9200  enfii  9223  ttrclselem2  9763  kmlem3  10190  cflem  10282  cflemOLD  10283  genpass  11046  ltexprlem4  11076  hasheqf1oi  14386  elwspths2spth  29996  bnj534  34731  bnj906  34922  bnj908  34923  bnj916  34925  bnj983  34943  bnj986  34947  fmla0  35366  fmlasuc0  35368  rexxfr3dALT  35623  dftr6  35730  bj-eeanvw  36695  bj-substw  36704  bj-csbsnlem  36885  bj-clel3gALT  37030  bj-rest10  37070  bj-restuni  37079  bj-imdirco  37172  bj-ccinftydisj  37195  wl-dfclab  37576  eldmqsres2  38269  disjdmqscossss  38784  prter2  38862  dihglb2  41324  prjspeclsp  42598  pm11.6  44387  pm11.71  44392  rfcnnnub  44973  eliunxp2  48178  thinccic  48861