Theorem 19.41v 1950

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  19.41vv  1951  19.41vvv  1952  19.41vvvv  1953  19.42v  1954  exdistrv  1956  r19.41v  3166  gencbvex  3499  euxfrw  3679  euxfr  3681  euind  3682  dfdif3OLD  4070  zfpair  5366  opabn0  5501  eliunxp  5786  relop  5799  dmuni  5863  dminss  6111  imainss  6112  cnvresima  6188  rnco  6210  rncoOLD  6211  coass  6224  xpco  6247  rnoprab  7463  eloprabga  7467  f11o  7891  frxp  8068  omeu  8512  domen  8898  xpassen  8999  enfii  9110  ttrclselem2  9635  kmlem3  10063  cflem  10155  cflemOLD  10156  genpass  10920  ltexprlem4  10950  hasheqf1oi  14274  elwspths2spth  30043  bnj534  34895  bnj906  35086  bnj908  35087  bnj916  35089  bnj983  35107  bnj986  35111  fmla0  35576  fmlasuc0  35578  rexxfr3dALT  35833  dftr6  35945  bj-eeanvw  36914  bj-substw  36923  bj-csbsnlem  37104  bj-clel3gALT  37249  bj-rest10  37293  bj-restuni  37302  bj-imdirco  37395  bj-ccinftydisj  37418  wl-dfclab  37790  eldmqsres2  38487  disjdmqscossss  39062  prter2  39141  dihglb2  41602  prjspeclsp  42855  pm11.6  44633  pm11.71  44638  rfcnnnub  45281  eliunxp2  48580  thinccic  49716