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  2567  rspn0  4297  relopabi  5771  lfuhgr3  35318  bj-cbveximdv  36944  bj-spvw  36945  bj-spvew  36946  bj-exextruan  36948  bj-cbvexvv  36950  bj-cbval  36956  bj-cbvexivw  36983  bj-eqs  36986  bj-nnfv  37081  bj-snsetex  37286  bj-snglss  37293  bj-axseprep  37397  bj-axreprepsep  37398  topdifinffinlem  37677  wl-eujustlem1  37927  ac6s6f  38508  ismnushort  44746  fnchoice  45478  ormklocald  47320  natlocalincr  47322