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  2093  sbequ2  2256  mo4  2566  rspn0  4308  relopabi  5771  lfuhgr3  35314  bj-cbvalim  36845  bj-cbvexim  36846  bj-cbvexivw  36873  bj-eqs  36876  bj-nnfv  36955  bj-snsetex  37164  bj-snglss  37171  bj-spvw  37274  bj-cbvexvv  37275  topdifinffinlem  37552  wl-eujustlem1  37793  ac6s6f  38374  ismnushort  44542  fnchoice  45274  ormklocald  47118  natlocalincr  47120