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  2254  mo4  2563  rspn0  4305  relopabi  5766  lfuhgr3  35185  bj-cbvalim  36710  bj-cbvexim  36711  bj-cbvexivw  36737  bj-eqs  36740  bj-nnfv  36819  bj-snsetex  37028  bj-snglss  37035  topdifinffinlem  37412  ac6s6f  38233  ismnushort  44418  fnchoice  45150  ormklocald  46996  natlocalincr  46998