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

Theorem ax5e 1915
Description: A rephrasing of ax-5 1913 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017.)
Assertion
Ref Expression
ax5e (∃𝑥𝜑𝜑)
Distinct variable group:   𝜑,𝑥

Proof of Theorem ax5e
StepHypRef Expression
1 ax-5 1913 . 2 𝜑 → ∀𝑥 ¬ 𝜑)
2 eximal 1784 . 2 ((∃𝑥𝜑𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
31, 2mpbir 230 1 (∃𝑥𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1539  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1913
This theorem depends on definitions:  df-bi 206  df-ex 1782
This theorem is referenced by:  ax5ea  1916  exlimiv  1933  exlimdv  1936  19.21v  1942  19.23v  1945  19.36imv  1948  19.36imvOLD  1949  19.41v  1953  19.9v  1987  aeveq  2059  sbv  2091  sbequ2  2241  mo4  2560  rspn0  4351  relopabi  5820  lfuhgr3  34098  bj-cbvalim  35510  bj-cbvexim  35511  bj-cbvexivw  35537  bj-eqs  35540  bj-nnfv  35620  bj-snsetex  35832  bj-snglss  35839  topdifinffinlem  36216  ac6s6f  37029  ismnushort  43045  fnchoice  43698  natlocalincr  45576
  Copyright terms: Public domain W3C validator