Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.41v Structured version   Visualization version   GIF version

Theorem 19.41v 1917
 Description: Version of 19.41 2141 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1945. (Revised by Rohan Ridenour, 15-Apr-2022.)
Assertion
Ref Expression
19.41v (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Distinct variable group:   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.41v
StepHypRef Expression
1 19.40 1837 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 ax5e 1881 . . . 4 (∃𝑥𝜓𝜓)
32anim2i 592 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑𝜓))
41, 3syl 17 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
5 pm3.21 463 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
65eximdv 1886 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
76impcom 445 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
84, 7impbii 199 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 383  ∃wex 1744 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745 This theorem is referenced by:  19.41vv  1918  19.41vvv  1919  19.41vvvv  1920  19.42v  1921  equsexvw  1978  r19.41v  3118  gencbvex  3281  euxfr  3425  euind  3426  zfpair  4934  opabn0  5035  eliunxp  5292  relop  5305  dmuni  5366  dmres  5454  dminss  5582  imainss  5583  ssrnres  5607  cnvresima  5661  resco  5677  rnco  5679  coass  5692  xpco  5713  rnoprab  6785  f11o  7170  frxp  7332  omeu  7710  domen  8010  xpassen  8095  kmlem3  9012  cflem  9106  genpass  9869  ltexprlem4  9899  hasheqf1oi  13180  elwspths2spth  26934  bnj534  30934  bnj906  31126  bnj908  31127  bnj916  31129  bnj983  31147  bnj986  31150  dftr6  31766  bj-eeanvw  32829  bj-cleljustab  32972  bj-csbsnlem  33023  bj-rest10  33166  bj-restuni  33175  bj-ccinftydisj  33230  eldmqsres2  34193  prter2  34485  dihglb2  36948  pm11.6  38909  pm11.71  38914  rfcnnnub  39509  eliunxp2  42437
 Copyright terms: Public domain W3C validator