Theorem ax5e 1915

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

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

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

This theorem depends on definitions:  df-bi 206  df-ex 1782

This theorem is referenced by:  ax5ea  1916  exlimiv  1933  exlimdv  1936  19.21v  1942  19.23v  1945  19.36imv  1948  19.36imvOLD  1949  19.41v  1953  19.9v  1987  aeveq  2059  sbv  2091  sbequ2  2241  mo4  2560  rspn0  4351  relopabi  5820  lfuhgr3  34098  bj-cbvalim  35510  bj-cbvexim  35511  bj-cbvexivw  35537  bj-eqs  35540  bj-nnfv  35620  bj-snsetex  35832  bj-snglss  35839  topdifinffinlem  36216  ac6s6f  37029  ismnushort  43045  fnchoice  43698  natlocalincr  45576