Theorem ax5e 1914

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

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

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

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

This theorem is referenced by:  ax5ea  1915  exlimiv  1932  exlimdv  1935  19.21v  1941  19.23v  1944  19.36imv  1947  19.41v  1951  19.9v  1986  aeveq  2060  sbv  2094  sbequ2  2257  mo4  2566  rspn0  4296  relopabi  5778  lfuhgr3  35302  bj-cbveximdv  36928  bj-spvw  36929  bj-spvew  36930  bj-exextruan  36932  bj-cbvexvv  36934  bj-cbval  36940  bj-cbvexivw  36967  bj-eqs  36970  bj-nnfv  37065  bj-snsetex  37270  bj-snglss  37277  bj-axseprep  37381  bj-axreprepsep  37382  topdifinffinlem  37663  wl-eujustlem1  37913  ac6s6f  38494  ismnushort  44728  fnchoice  45460  ormklocald  47304  natlocalincr  47306