Theorem 19.41v 1972

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

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

This theorem is referenced by:  19.41vv  1973  19.41vvv  1974  19.41vvvv  1975  19.42v  1976  exdistrv  1978  r19.41v  3195  gencbvex  3513  euxfrw  3687  euxfr  3689  euind  3690  dfdif3OLD  4075  zfpair  5382  opabn0  5528  eliunxp  5813  relop  5826  dmuni  5894  dminss  6141  imainss  6142  cnvresima  6220  rnco  6242  rncoOLD  6243  coass  6256  xpco  6279  rnoprab  7505  eloprabga  7509  f11o  7932  frxp  8110  omeu  8558  domen  8946  xpassen  9047  enfii  9158  ttrclselem2  9683  kmlem3  10124  cflem  10216  cflemOLD  10217  genpass  10982  ltexprlem4  11012  hasheqf1oi  14375  elwspths2spth  30224  bnj534  35040  bnj906  35230  bnj908  35231  bnj916  35233  bnj983  35251  bnj986  35255  fmla0  35740  fmlasuc0  35742  rexxfr3dALT  35997  dftr6  36109  bj-eeanvw  37197  bj-substw  37207  bj-csbsnlem  37395  bj-clel3gALT  37540  bj-rest10  37585  bj-restuni  37594  bj-imdirco  37689  bj-ccinftydisj  37712  wl-dfclab  38095  eldmqsres2  38800  disjdmqscossss  39412  prter2  39512  dihglb2  41973  prjspeclsp  43201  pm11.6  44961  pm11.71  44966  rfcnnnub  45615  eliunxp2  48966  thinccic  50101