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 1924
Description: Version of 19.23 2178 with a disjoint variable 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 1951. (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 1819 . . 3 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 ax5e 1894 . . 3 (∃𝑥𝜓𝜓)
31, 2syl6 35 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
4 ax-5 1892 . . . 4 (𝜓 → ∀𝑥𝜓)
54imim2i 16 . . 3 ((∃𝑥𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6 19.38 1824 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
75, 6syl 17 . 2 ((∃𝑥𝜑𝜓) → ∀𝑥(𝜑𝜓))
83, 7impbii 210 1 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1523  wex 1765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892
This theorem depends on definitions:  df-bi 208  df-ex 1766
This theorem is referenced by:  19.23vv  1925  pm11.53v  1926  equsv  1990  sbequ2  2216  sb4b  2459  2mo2  2704  euind  3654  reuind  3683  unissb  4782  disjor  4950  dftr2  5072  ssrelrel  5562  cotrg  5854  dffun2  6242  fununi  6306  dff13  6885  dffi2  8740  aceq2  9398  psgnunilem4  18360  metcld  23596  metcld2  23597  isch2  28687  disjorf  30015  funcnv5mpt  30099  bnj1052  31857  bnj1030  31869  dfon2lem8  32645  bj-ssbeq  33590  bj-ssbid2ALT  33600  bj-sblem1  33742  bj-sblem2  33743  bj-sblem  33744  wl-equsalvw  34331  ineleq  35161  cocossss  35233  cossssid3  35261  trcoss2  35276  elmapintrab  39442  elinintrab  39443  undmrnresiss  39470  elintima  39504  relexp0eq  39552  dfhe3  39627  ismnuprim  40148  pm10.52  40256  truniALT  40435  tpid3gVD  40736  truniALTVD  40772  onfrALTVD  40785  unisnALT  40820
  Copyright terms: Public domain W3C validator