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 2020
Description: Version of 19.23 2227 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 2054. (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 1910 . . 3 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 ax5e 1990 . . 3 (∃𝑥𝜓𝜓)
31, 2syl6 35 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
4 ax-5 1988 . . . 4 (𝜓 → ∀𝑥𝜓)
54imim2i 16 . . 3 ((∃𝑥𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6 19.38 1915 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
75, 6syl 17 . 2 ((∃𝑥𝜑𝜓) → ∀𝑥(𝜑𝜓))
83, 7impbii 199 1 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1630  wex 1853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988
This theorem depends on definitions:  df-bi 197  df-ex 1854
This theorem is referenced by:  19.23vv  2021  pm11.53v  2071  equsalvw  2086  2mo2  2688  euind  3534  reuind  3552  unissb  4621  disjor  4786  dftr2  4906  ssrelrel  5377  cotrg  5665  dffun2  6059  fununi  6125  dff13  6676  dffi2  8496  aceq2  9152  psgnunilem4  18137  metcld  23324  metcld2  23325  isch2  28410  disjorf  29720  funcnv5mpt  29799  bnj1052  31371  bnj1030  31383  dfon2lem8  32021  bj-ssbeq  32955  bj-ssb0  32956  bj-ssb1a  32960  bj-ssb1  32961  bj-ssbequ2  32971  bj-ssbid2ALT  32974  ineleq  34460  cocossss  34532  cossssid3  34560  trcoss2  34575  elmapintrab  38402  elinintrab  38403  undmrnresiss  38430  elintima  38465  relexp0eq  38513  dfhe3  38589  pm10.52  39084  truniALT  39271  tpid3gVD  39594  truniALTVD  39631  onfrALTVD  39644  unisnALT  39679
  Copyright terms: Public domain W3C validator