Theorem ax5e 1910

Description: A rephrasing of ax-5 1908 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 1908	. 2 ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)
2		eximal 1779	. 2 ⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
3	1, 2	mpbir 231	1 ⊢ (∃𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1535  ∃wex 1776

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

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

This theorem is referenced by:  ax5ea  1911  exlimiv  1928  exlimdv  1931  19.21v  1937  19.23v  1940  19.36imv  1943  19.41v  1947  19.9v  1981  aeveq  2054  sbv  2086  sbequ2  2247  mo4  2564  rspn0  4362  relopabi  5835  lfuhgr3  35104  bj-cbvalim  36628  bj-cbvexim  36629  bj-cbvexivw  36655  bj-eqs  36658  bj-nnfv  36737  bj-snsetex  36946  bj-snglss  36953  topdifinffinlem  37330  ac6s6f  38160  ismnushort  44297  fnchoice  44967  natlocalincr  46830