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 1899
Description: Version of 19.23 2078 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 1758 . . 3 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 19.9v 1893 . . 3 (∃𝑥𝜓𝜓)
31, 2syl6ib 241 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
4 ax-5 1836 . . . 4 (𝜓 → ∀𝑥𝜓)
54imim2i 16 . . 3 ((∃𝑥𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6 19.38 1763 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
75, 6syl 17 . 2 ((∃𝑥𝜑𝜓) → ∀𝑥(𝜑𝜓))
83, 7impbii 199 1 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1478  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  19.23vv  1900  pm11.53v  1903  equsalvw  1928  2mo2  2549  euind  3375  reuind  3393  unissb  4435  disjor  4597  dftr2  4714  ssrelrel  5181  cotrg  5466  dffun2  5857  fununi  5922  dff13  6466  dffi2  8273  aceq2  8886  psgnunilem4  17838  metcld  23012  metcld2  23013  isch2  27929  disjorf  29237  funcnv5mpt  29312  bnj1052  30751  bnj1030  30763  dfon2lem8  31396  bj-ssbeq  32269  bj-ssb0  32270  bj-ssb1a  32274  bj-ssb1  32275  bj-ssbequ2  32285  bj-ssbid2ALT  32288  elmapintrab  37363  elinintrab  37364  undmrnresiss  37391  elintima  37426  relexp0eq  37474  dfhe3  37551  pm10.52  38046  truniALT  38233  tpid3gVD  38560  truniALTVD  38597  onfrALTVD  38610  unisnALT  38645
  Copyright terms: Public domain W3C validator