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

Theorem ax5e 1912
Description: A rephrasing of ax-5 1910 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 1910 . 2 𝜑 → ∀𝑥 ¬ 𝜑)
2 eximal 1782 . 2 ((∃𝑥𝜑𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
31, 2mpbir 231 1 (∃𝑥𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1538  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  ax5ea  1913  exlimiv  1930  exlimdv  1933  19.21v  1939  19.23v  1942  19.36imv  1945  19.41v  1949  19.9v  1983  aeveq  2056  sbv  2088  sbequ2  2249  mo4  2566  rspn0  4356  relopabi  5832  lfuhgr3  35125  bj-cbvalim  36646  bj-cbvexim  36647  bj-cbvexivw  36673  bj-eqs  36676  bj-nnfv  36755  bj-snsetex  36964  bj-snglss  36971  topdifinffinlem  37348  ac6s6f  38180  ismnushort  44320  fnchoice  45034  ormklocald  46889  natlocalincr  46891
  Copyright terms: Public domain W3C validator