Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.23v Structured version   Visualization version   GIF version

Theorem 19.23v 1943
 Description: Version of 19.23 2209 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 1970. (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 1835 . . 3 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 ax5e 1913 . . 3 (∃𝑥𝜓𝜓)
31, 2syl6 35 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
4 ax-5 1911 . . . 4 (𝜓 → ∀𝑥𝜓)
54imim2i 16 . . 3 ((∃𝑥𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6 19.38 1840 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
75, 6syl 17 . 2 ((∃𝑥𝜑𝜓) → ∀𝑥(𝜑𝜓))
83, 7impbii 212 1 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  ∃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 1911 This theorem depends on definitions:  df-bi 210  df-ex 1782 This theorem is referenced by:  19.23vv  1944  pm11.53v  1945  equsv  2009  sbequ2OLD  2248  sb4b  2488  sb4bOLD  2489  2mo2  2709  euind  3663  reuind  3692  unissb  4833  disjor  5011  dftr2  5139  ssrelrel  5634  cotrg  5939  dffun2  6337  fununi  6402  dff13  6996  dffi2  8878  aceq2  9537  psgnunilem4  18625  metcld  23924  metcld2  23925  isch2  29020  disjorf  30356  funcnv5mpt  30445  bnj1052  32393  bnj1030  32405  dfon2lem8  33184  bj-ssbeq  34139  bj-ssbid2ALT  34149  bj-sblem1  34321  bj-sblem2  34322  bj-sblem  34323  wl-equsalvw  34983  ineleq  35808  cocossss  35881  cossssid3  35909  trcoss2  35924  elmapintrab  40340  elinintrab  40341  undmrnresiss  40368  elintima  40418  relexp0eq  40466  dfhe3  40540  ismnuprim  41066  pm10.52  41133  truniALT  41311  tpid3gVD  41612  truniALTVD  41648  onfrALTVD  41661  unisnALT  41696
 Copyright terms: Public domain W3C validator