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  4310  relopabi  5779  lfuhgr3  35333  bj-spvw  36872  bj-spvew  36873  bj-exextruan  36875  bj-cbvexvv  36877  bj-cbvalim  36883  bj-cbvexim  36884  bj-cbvexivw  36911  bj-eqs  36914  bj-nnfv  37005  bj-snsetex  37205  bj-snglss  37212  bj-axseprep  37316  bj-axreprepsep  37317  topdifinffinlem  37596  wl-eujustlem1  37837  ac6s6f  38418  ismnushort  44651  fnchoice  45383  ormklocald  47226  natlocalincr  47228