Theorem 19.41v 1956

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

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

This theorem is referenced by:  19.41vv  1957  19.41vvv  1958  19.41vvvv  1959  19.42v  1960  exdistrv  1962  r19.41v  3169  gencbvex  3488  euxfrw  3662  euxfr  3664  euind  3665  dfdif3OLD  4049  zfpair  5350  opabn0  5495  eliunxp  5779  relop  5792  dmuni  5856  dminss  6104  imainss  6105  cnvresima  6181  rnco  6203  rncoOLD  6204  coass  6217  xpco  6240  rnoprab  7461  eloprabga  7465  f11o  7889  frxp  8066  omeu  8510  domen  8898  xpassen  8999  enfii  9110  ttrclselem2  9638  kmlem3  10066  cflem  10158  cflemOLD  10159  genpass  10923  ltexprlem4  10953  hasheqf1oi  14304  elwspths2spth  30056  bnj534  34922  bnj906  35112  bnj908  35113  bnj916  35115  bnj983  35133  bnj986  35137  fmla0  35610  fmlasuc0  35612  rexxfr3dALT  35867  dftr6  35979  bj-eeanvw  37058  bj-substw  37068  bj-csbsnlem  37256  bj-clel3gALT  37401  bj-rest10  37446  bj-restuni  37455  bj-imdirco  37550  bj-ccinftydisj  37573  wl-dfclab  37956  eldmqsres2  38661  disjdmqscossss  39273  prter2  39373  dihglb2  41834  prjspeclsp  43062  pm11.6  44836  pm11.71  44841  rfcnnnub  45484  eliunxp2  48825  thinccic  49961