Theorem 19.41v 1953

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  19.41vv  1954  19.41vvv  1955  19.41vvvv  1956  19.42v  1957  exdistrv  1959  r19.41v  3188  gencbvex  3535  euxfrw  3717  euxfr  3719  euind  3720  dfdif3  4114  zfpair  5419  opabn0  5553  eliunxp  5837  relop  5850  dmuni  5914  dminss  6152  imainss  6153  cnvresima  6229  rnco  6251  coass  6264  xpco  6288  rnoprab  7511  eloprabga  7515  f11o  7932  frxp  8111  omeu  8584  domen  8956  xpassen  9065  dif1enOLD  9161  enfii  9188  ttrclselem2  9720  kmlem3  10146  cflem  10240  genpass  11003  ltexprlem4  11033  hasheqf1oi  14310  elwspths2spth  29218  bnj534  33745  bnj906  33936  bnj908  33937  bnj916  33939  bnj983  33957  bnj986  33961  fmla0  34368  fmlasuc0  34370  dftr6  34716  bj-eeanvw  35586  bj-substw  35595  bj-csbsnlem  35778  bj-clel3gALT  35924  bj-rest10  35964  bj-restuni  35973  bj-imdirco  36066  bj-ccinftydisj  36089  wl-dfclab  36453  eldmqsres2  37151  disjdmqscossss  37668  prter2  37746  dihglb2  40208  prjspeclsp  41355  pm11.6  43141  pm11.71  43146  rfcnnnub  43710  eliunxp2  46999  thinccic  47671