Theorem 19.41v 2044

Description: Version of 19.41 2268 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 2070. (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 1967	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 2007	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 610	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 463	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 2012	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 396	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 200	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 197   ∧ wa 384  ∃wex 1874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875

This theorem is referenced by:  19.41vv  2045  19.41vvv  2046  19.41vvvv  2047  19.42v  2048  exdistrv  2050  equsexvw  2102  r19.41v  3236  gencbvex  3403  euxfr  3553  euind  3554  dfdif3  3884  zfpair  5062  opabn0  5169  eliunxp  5430  relop  5443  dmuni  5504  dminss  5732  imainss  5733  cnvresima  5811  rnco  5829  coass  5842  xpco  5863  rnoprab  6943  f11o  7328  frxp  7491  omeu  7872  domen  8175  xpassen  8263  kmlem3  9229  cflem  9323  genpass  10086  ltexprlem4  10116  hasheqf1oi  13347  elwspths2spth  27195  bnj534  31260  bnj906  31451  bnj908  31452  bnj916  31454  bnj983  31472  bnj986  31475  dftr6  32088  bj-eeanvw  33142  bj-cleljustab  33279  bj-csbsnlem  33326  bj-rest10  33472  bj-restuni  33481  bj-ccinftydisj  33537  wl-dv-sb  33758  eldmqsres2  34487  prter2  34840  dihglb2  37301  pm11.6  39269  pm11.71  39274  rfcnnnub  39850  eliunxp2  42784