Theorem 19.41v 1979

Description: Version of 19.41 2271 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1997. (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 1916	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1942	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 628	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 18	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 476	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1947	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 412	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 212	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  19.41vv  1980  19.41vvv  1981  19.41vvvv  1982  19.42v  1983  exdistrv  1985  r19.41v  3195  gencbvex  3511  euxfrw  3685  euxfr  3687  euind  3688  dfdif3OLD  4074  zfpair  5394  opabn0  5540  eliunxp  5825  relop  5838  dmuni  5906  dminss  6152  imainss  6153  cnvresima  6233  rnco  6255  rncoOLD  6256  coass  6269  xpco  6292  rnoprab  7517  eloprabga  7521  f11o  7945  frxp  8123  omeu  8571  domen  8959  xpassen  9060  enfii  9171  ttrclselem2  9696  kmlem3  10137  cflem  10229  cflemOLD  10230  genpass  10995  ltexprlem4  11025  hasheqf1oi  14389  elwspths2spth  30300  bnj534  35109  bnj906  35299  bnj908  35300  bnj916  35302  bnj983  35320  bnj986  35324  fmla0  35855  fmlasuc0  35857  rexxfr3dALT  36112  dftr6  36224  bj-eeanvw  37321  bj-substw  37331  bj-csbsnlem  37519  bj-clel3gALT  37665  bj-rest10  37711  bj-restuni  37720  bj-imdirco  37815  bj-ccinftydisj  37838  wl-dfclab  38221  eldmqsres2  38924  disjdmqscossss  39536  prter2  39636  dihglb2  42097  prjspeclsp  43327  pm11.6  45085  pm11.71  45090  rfcnnnub  45739  eliunxp2  49097  thinccic  50232