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 1945
Description: Version of 19.23 2204 with a disjoint variable condition instead of a nonfreeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.) Remove dependency on ax-6 1971. (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 1836 . . 3 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 ax5e 1915 . . 3 (∃𝑥𝜓𝜓)
31, 2syl6 35 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
4 ax-5 1913 . . . 4 (𝜓 → ∀𝑥𝜓)
54imim2i 16 . . 3 ((∃𝑥𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6 19.38 1841 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
75, 6syl 17 . 2 ((∃𝑥𝜑𝜓) → ∀𝑥(𝜑𝜓))
83, 7impbii 208 1 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1539  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913
This theorem depends on definitions:  df-bi 206  df-ex 1782
This theorem is referenced by:  19.23vv  1946  pm11.53v  1947  equsv  2006  sb4b  2473  sb4bOLD  2474  2mo2  2647  ceqsalv  3480  clel2g  3608  clel4g  3613  elabd2  3621  elabgt  3623  elabg  3627  euind  3681  reuind  3710  sbcg  3817  ralsng  4633  snssb  4742  unissb  4899  unissbOLD  4900  disjor  5084  dftr2  5223  ssrelrel  5751  cotrg  6060  cotrgOLD  6061  cotrgOLDOLD  6062  dffun2OLDOLD  6506  fununi  6574  dff13  7199  dffi2  9356  aceq2  10052  psgnunilem4  19275  metcld  24666  metcld2  24667  isch2  30063  disjorf  31395  funcnv5mpt  31482  bnj1052  33478  bnj1030  33490  dfon2lem8  34257  bj-ssbeq  35106  bj-ssbid2ALT  35116  bj-sblem1  35297  bj-sblem2  35298  bj-sblem  35299  wl-equsalvw  35986  ineleq  36804  cocossss  36887  cossssid3  36920  trcoss2  36935  elmapintrab  41828  elinintrab  41829  undmrnresiss  41856  elintima  41905  relexp0eq  41953  dfhe3  42027  ismnuprim  42554  pm10.52  42625  truniALT  42803  tpid3gVD  43104  truniALTVD  43140  onfrALTVD  43153  unisnALT  43188
  Copyright terms: Public domain W3C validator