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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1537  ∃wex 1782

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 1783

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  2566  rspn0  4286  relopabi  5732  lfuhgr3  33081  bj-cbvalim  34826  bj-cbvexim  34827  bj-cbvexivw  34853  bj-eqs  34856  bj-nnfv  34936  bj-snsetex  35153  bj-snglss  35160  topdifinffinlem  35518  ac6s6f  36331  ismnushort  41919  fnchoice  42572  natlocalincr  46511