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 2023
Description: Version of 19.23 2236 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 2057. (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 1909 . . 3 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 ax5e 1993 . . 3 (∃𝑥𝜓𝜓)
31, 2syl6 35 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
4 ax-5 1991 . . . 4 (𝜓 → ∀𝑥𝜓)
54imim2i 16 . . 3 ((∃𝑥𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6 19.38 1914 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
75, 6syl 17 . 2 ((∃𝑥𝜑𝜓) → ∀𝑥(𝜑𝜓))
83, 7impbii 199 1 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1629  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-ex 1853
This theorem is referenced by:  19.23vv  2024  pm11.53v  2074  equsalvw  2089  2mo2  2699  euind  3545  reuind  3563  unissb  4605  disjor  4768  dftr2  4888  ssrelrel  5360  cotrg  5648  dffun2  6041  fununi  6104  dff13  6655  dffi2  8485  aceq2  9142  psgnunilem4  18124  metcld  23323  metcld2  23324  isch2  28420  disjorf  29730  funcnv5mpt  29809  bnj1052  31381  bnj1030  31393  dfon2lem8  32031  bj-ssbeq  32965  bj-ssb0  32966  bj-ssb1a  32970  bj-ssb1  32971  bj-ssbequ2  32980  bj-ssbid2ALT  32983  ineleq  34461  cocossss  34533  cossssid3  34561  trcoss2  34576  elmapintrab  38408  elinintrab  38409  undmrnresiss  38436  elintima  38471  relexp0eq  38519  dfhe3  38595  pm10.52  39090  truniALT  39276  tpid3gVD  39599  truniALTVD  39636  onfrALTVD  39649  unisnALT  39684
  Copyright terms: Public domain W3C validator