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

Theorem 19.23v 1901
Description: Version of 19.23 2079 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 1760 . . 3 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 19.9v 1895 . . 3 (∃𝑥𝜓𝜓)
31, 2syl6ib 241 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
4 ax-5 1838 . . . 4 (𝜓 → ∀𝑥𝜓)
54imim2i 16 . . 3 ((∃𝑥𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6 19.38 1765 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
75, 6syl 17 . 2 ((∃𝑥𝜑𝜓) → ∀𝑥(𝜑𝜓))
83, 7impbii 199 1 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1480  wex 1703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887
This theorem depends on definitions:  df-bi 197  df-ex 1704
This theorem is referenced by:  19.23vv  1902  pm11.53v  1905  equsalvw  1930  2mo2  2549  euind  3391  reuind  3409  unissb  4467  disjor  4632  dftr2  4752  ssrelrel  5218  cotrg  5505  dffun2  5896  fununi  5962  dff13  6509  dffi2  8326  aceq2  8939  psgnunilem4  17911  metcld  23098  metcld2  23099  isch2  28064  disjorf  29376  funcnv5mpt  29454  bnj1052  31028  bnj1030  31040  dfon2lem8  31679  bj-ssbeq  32611  bj-ssb0  32612  bj-ssb1a  32616  bj-ssb1  32617  bj-ssbequ2  32627  bj-ssbid2ALT  32630  elmapintrab  37708  elinintrab  37709  undmrnresiss  37736  elintima  37771  relexp0eq  37819  dfhe3  37895  pm10.52  38390  truniALT  38577  tpid3gVD  38903  truniALTVD  38940  onfrALTVD  38953  unisnALT  38988
  Copyright terms: Public domain W3C validator