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

Theorem 19.23v 1889
 Description: Version of 19.23 2067 with a dv condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.)
Assertion
Ref Expression
19.23v (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Distinct variable group:   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.23v
StepHypRef Expression
1 exim 1751 . . 3 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 19.9v 1883 . . 3 (∃𝑥𝜓𝜓)
31, 2syl6ib 240 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
4 ax-5 1827 . . . 4 (𝜓 → ∀𝑥𝜓)
54imim2i 16 . . 3 ((∃𝑥𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6 19.38 1757 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
75, 6syl 17 . 2 ((∃𝑥𝜑𝜓) → ∀𝑥(𝜑𝜓))
83, 7impbii 198 1 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473  ∃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-ex 1696 This theorem is referenced by:  19.23vv  1890  pm11.53v  1893  equsalvw  1918  2mo2  2538  euind  3360  reuind  3378  unissb  4405  disjor  4567  dftr2  4682  ssrelrel  5143  cotrg  5426  dffun2  5814  fununi  5878  dff13  6416  dffi2  8212  aceq2  8825  psgnunilem4  17740  metcld  22912  metcld2  22913  isch2  27464  disjorf  28774  funcnv5mpt  28852  bnj1052  30297  bnj1030  30309  dfon2lem8  30939  bj-ssbeq  31816  bj-ssb0  31817  bj-ssb1a  31821  bj-ssb1  31822  bj-ssbequ2  31832  bj-ssbid2ALT  31835  elmapintrab  36901  elinintrab  36902  undmrnresiss  36929  elintima  36964  relexp0eq  37012  dfhe3  37089  pm10.52  37586  truniALT  37772  tpid3gVD  38099  truniALTVD  38136  onfrALTVD  38149  unisnALT  38184
 Copyright terms: Public domain W3C validator