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 2034
Description: Version of 19.23 2248 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.) Remove dependency on ax-6 2069. (Revised by Rohan Ridenour, 15-Apr-2022.)
Assertion
Ref Expression
19.23v (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Distinct variable group:   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.23v
StepHypRef Expression
1 exim 1918 . . 3 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 ax5e 2003 . . 3 (∃𝑥𝜓𝜓)
31, 2syl6 35 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
4 ax-5 2001 . . . 4 (𝜓 → ∀𝑥𝜓)
54imim2i 16 . . 3 ((∃𝑥𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6 19.38 1923 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
75, 6syl 17 . 2 ((∃𝑥𝜑𝜓) → ∀𝑥(𝜑𝜓))
83, 7impbii 200 1 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wal 1635  wex 1859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-ex 1860
This theorem is referenced by:  19.23vv  2035  pm11.53v  2086  equsalvw  2101  2mo2  2725  euind  3602  reuind  3620  unissb  4674  disjor  4837  dftr2  4959  ssrelrel  5436  cotrg  5731  dffun2  6121  fununi  6185  dff13  6746  dffi2  8578  aceq2  9235  psgnunilem4  18138  metcld  23338  metcld2  23339  isch2  28431  disjorf  29740  funcnv5mpt  29819  bnj1052  31388  bnj1030  31400  dfon2lem8  32037  bj-ssbeq  32965  bj-ssb0  32966  bj-ssb1a  32970  bj-ssb1  32971  bj-ssbequ2  32980  bj-ssbid2ALT  32983  ineleq  34451  cocossss  34523  cossssid3  34551  trcoss2  34566  elmapintrab  38400  elinintrab  38401  undmrnresiss  38428  elintima  38463  relexp0eq  38511  dfhe3  38587  pm10.52  39082  truniALT  39267  tpid3gVD  39589  truniALTVD  39626  onfrALTVD  39639  unisnALT  39674
  Copyright terms: Public domain W3C validator