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

Theorem 19.41v 1900
Description: Version of 19.41 2089 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 1784 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 19.9v 1882 . . . 4 (∃𝑥𝜓𝜓)
32anbi2i 725 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑𝜓))
41, 3sylib 206 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
5 pm3.21 462 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
65eximdv 1832 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
76impcom 444 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
84, 7impbii 197 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  19.41vv  1901  19.41vvv  1902  19.41vvvv  1903  19.42v  1904  equsexvw  1918  r19.41v  3069  gencbvex  3222  euxfr  3358  euind  3359  zfpair  4826  opabn0  4921  eliunxp  5169  relop  5182  dmuni  5243  dmres  5326  dminss  5452  imainss  5453  ssrnres  5477  cnvresima  5527  resco  5542  rnco  5544  coass  5557  xpco  5578  rnoprab  6619  f11o  6999  frxp  7152  omeu  7530  domen  7832  xpassen  7917  kmlem3  8835  cflem  8929  genpass  9688  ltexprlem4  9718  hasheqf1oi  12957  hasheqf1oiOLD  12958  3v3e3cycl2  25986  bnj534  29896  bnj906  30088  bnj908  30089  bnj916  30091  bnj983  30109  bnj986  30112  dftr6  30727  bj-eeanvw  31725  bj-csbsnlem  31914  bj-rest10  32046  bj-restuni  32055  bj-ccinftydisj  32101  prter2  33008  dihglb2  35473  pm11.6  37438  pm11.71  37443  rfcnnnub  38042  elwspths2spth  41193  eliunxp2  41927
  Copyright terms: Public domain W3C validator