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

Theorem 19.41v 1901
 Description: Version of 19.41 2090 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
19.41v (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Distinct variable group:   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.41v
StepHypRef Expression
1 19.40 1785 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 19.9v 1883 . . . 4 (∃𝑥𝜓𝜓)
32anbi2i 726 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑𝜓))
41, 3sylib 207 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
5 pm3.21 463 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
65eximdv 1833 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
76impcom 445 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
84, 7impbii 198 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696 This theorem is referenced by:  19.41vv  1902  19.41vvv  1903  19.41vvvv  1904  19.42v  1905  equsexvw  1919  r19.41v  3070  gencbvex  3223  euxfr  3359  euind  3360  zfpair  4831  opabn0  4931  eliunxp  5181  relop  5194  dmuni  5256  dmres  5339  dminss  5466  imainss  5467  ssrnres  5491  cnvresima  5541  resco  5556  rnco  5558  coass  5571  xpco  5592  rnoprab  6641  f11o  7021  frxp  7174  omeu  7552  domen  7854  xpassen  7939  kmlem3  8857  cflem  8951  genpass  9710  ltexprlem4  9740  hasheqf1oi  13002  hasheqf1oiOLD  13003  3v3e3cycl2  26192  bnj534  30062  bnj906  30254  bnj908  30255  bnj916  30257  bnj983  30275  bnj986  30278  dftr6  30893  bj-eeanvw  31891  bj-csbsnlem  32090  bj-rest10  32222  bj-restuni  32231  bj-ccinftydisj  32277  prter2  33184  dihglb2  35649  pm11.6  37614  pm11.71  37619  rfcnnnub  38218  elwspths2spth  41171  eliunxp2  41905
 Copyright terms: Public domain W3C validator