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 1784	. 2 ⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
3	1, 2	mpbir 234	1 ⊢ (∃𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1536  ∃wex 1781

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 210  df-ex 1782

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  1988  aeveq  2061  sbv  2095  sbequ2  2247  mo4  2625  rspn0  4266  relopabi  5658  lfuhgr3  32479  bj-cbvalim  34091  bj-cbvexim  34092  bj-cbvexivw  34118  bj-eqs  34121  bj-nnfv  34198  bj-snsetex  34399  bj-snglss  34406  topdifinffinlem  34764  ac6s6f  35611  fnchoice  41658