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

Theorem ax5e 1916
Description: A rephrasing of ax-5 1914 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 1914 . 2 𝜑 → ∀𝑥 ¬ 𝜑)
2 eximal 1785 . 2 ((∃𝑥𝜑𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
31, 2mpbir 230 1 (∃𝑥𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1540  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  ax5ea  1917  exlimiv  1934  exlimdv  1937  19.21v  1943  19.23v  1946  19.36imv  1949  19.36imvOLD  1950  19.41v  1954  19.9v  1988  aeveq  2060  sbv  2092  sbequ2  2242  mo4  2565  rspn0  4317  relopabi  5783  lfuhgr3  33753  bj-cbvalim  35138  bj-cbvexim  35139  bj-cbvexivw  35165  bj-eqs  35168  bj-nnfv  35248  bj-snsetex  35463  bj-snglss  35470  topdifinffinlem  35847  ac6s6f  36661  ismnushort  42655  fnchoice  43308  natlocalincr  45189
  Copyright terms: Public domain W3C validator