Theorem 19.41v 1950

Description: Version of 19.41 2240 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  3163  gencbvex  3496  euxfrw  3676  euxfr  3678  euind  3679  dfdif3OLD  4067  zfpair  5363  opabn0  5498  eliunxp  5783  relop  5796  dmuni  5860  dminss  6107  imainss  6108  cnvresima  6184  rnco  6206  rncoOLD  6207  coass  6220  xpco  6243  rnoprab  7459  eloprabga  7463  f11o  7887  frxp  8064  omeu  8508  domen  8892  xpassen  8993  enfii  9104  ttrclselem2  9625  kmlem3  10053  cflem  10145  cflemOLD  10146  genpass  10909  ltexprlem4  10939  hasheqf1oi  14262  elwspths2spth  29952  bnj534  34774  bnj906  34965  bnj908  34966  bnj916  34968  bnj983  34986  bnj986  34990  fmla0  35449  fmlasuc0  35451  rexxfr3dALT  35706  dftr6  35818  bj-eeanvw  36780  bj-substw  36789  bj-csbsnlem  36970  bj-clel3gALT  37115  bj-rest10  37155  bj-restuni  37164  bj-imdirco  37257  bj-ccinftydisj  37280  wl-dfclab  37652  eldmqsres2  38349  disjdmqscossss  38924  prter2  39003  dihglb2  41464  prjspeclsp  42733  pm11.6  44512  pm11.71  44517  rfcnnnub  45160  eliunxp2  48461  thinccic  49599