Theorem ax5e 1913

Description: A rephrasing of ax-5 1911 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017.)

Assertion

Ref	Expression
ax5e	⊢ (∃𝑥𝜑 → 𝜑)

Distinct variable group:   𝜑,𝑥

Proof of Theorem ax5e

Step	Hyp	Ref	Expression
1		ax-5 1911	. 2 ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)
2		eximal 1783	. 2 ⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
3	1, 2	mpbir 231	1 ⊢ (∃𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  ax5ea  1914  exlimiv  1931  exlimdv  1934  19.21v  1940  19.23v  1943  19.36imv  1946  19.41v  1950  19.9v  1985  aeveq  2059  sbv  2091  sbequ2  2252  mo4  2561  rspn0  4306  relopabi  5762  lfuhgr3  35152  bj-cbvalim  36678  bj-cbvexim  36679  bj-cbvexivw  36705  bj-eqs  36708  bj-nnfv  36787  bj-snsetex  36996  bj-snglss  37003  topdifinffinlem  37380  ac6s6f  38212  ismnushort  44333  fnchoice  45065  ormklocald  46911  natlocalincr  46913