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

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

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  2561  rspn0  4353  relopabi  5823  lfuhgr3  34110  bj-cbvalim  35522  bj-cbvexim  35523  bj-cbvexivw  35549  bj-eqs  35552  bj-nnfv  35632  bj-snsetex  35844  bj-snglss  35851  topdifinffinlem  36228  ac6s6f  37041  ismnushort  43060  fnchoice  43713  natlocalincr  45590