Theorem 19.41v 1927

Description: Version of 19.41 2202 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1947. (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 1868	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1890	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 616	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 472	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1895	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 408	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 210	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762

This theorem is referenced by:  19.41vv  1928  19.41vvv  1929  19.41vvvv  1930  19.42v  1931  exdistrv  1933  equsexvwOLD  1989  r19.41v  3308  gencbvex  3492  euxfr  3648  euind  3649  dfdif3  4012  zfpair  5213  opabn0  5328  eliunxp  5594  relop  5607  dmuni  5669  dminss  5886  imainss  5887  cnvresima  5962  rnco  5980  coass  5993  xpco  6015  rnoprab  7113  f11o  7504  frxp  7673  omeu  8061  domen  8370  xpassen  8458  kmlem3  9424  cflem  9514  genpass  10277  ltexprlem4  10307  hasheqf1oi  13562  elwspths2spth  27433  bnj534  31627  bnj906  31818  bnj908  31819  bnj916  31821  bnj983  31839  bnj986  31842  fmla0  32237  fmlasuc0  32239  dftr6  32594  bj-eeanvw  33646  bj-csbsnlem  33791  bj-rest10  33978  bj-restuni  33987  bj-ccinftydisj  34053  wl-dfclab  34359  eldmqsres2  35076  prter2  35548  dihglb2  38009  prjspeclsp  38759  pm11.6  40262  pm11.71  40267  rfcnnnub  40832  eliunxp2  43860