Theorem 19.41v 1946

Description: Version of 19.41 2224 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 1882	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1908	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 615	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 470	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1913	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 406	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 208	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 394  ∃wex 1774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775

This theorem is referenced by:  19.41vv  1947  19.41vvv  1948  19.41vvvv  1949  19.42v  1950  exdistrv  1952  r19.41v  3179  gencbvex  3527  euxfrw  3715  euxfr  3717  euind  3718  dfdif3  4113  zfpair  5425  opabn0  5559  eliunxp  5844  relop  5857  dmuni  5921  dminss  6164  imainss  6165  cnvresima  6241  rnco  6263  coass  6276  xpco  6300  rnoprab  7529  eloprabga  7533  f11o  7960  frxp  8140  omeu  8615  domen  8992  xpassen  9104  dif1enOLD  9200  enfii  9223  ttrclselem2  9769  kmlem3  10195  cflem  10289  genpass  11052  ltexprlem4  11082  hasheqf1oi  14368  elwspths2spth  29901  bnj534  34584  bnj906  34775  bnj908  34776  bnj916  34778  bnj983  34796  bnj986  34800  fmla0  35210  fmlasuc0  35212  rexxfr3dALT  35467  dftr6  35573  bj-eeanvw  36418  bj-substw  36427  bj-csbsnlem  36609  bj-clel3gALT  36755  bj-rest10  36795  bj-restuni  36804  bj-imdirco  36897  bj-ccinftydisj  36920  wl-dfclab  37291  eldmqsres2  37986  disjdmqscossss  38501  prter2  38579  dihglb2  41041  prjspeclsp  42266  pm11.6  44066  pm11.71  44071  rfcnnnub  44635  eliunxp2  47712  thinccic  48382