Theorem ax5e 1919

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1545  ∃wex 1786

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

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  ax5ea  1920  exlimiv  1937  exlimdv  1940  19.21v  1946  19.23v  1949  19.36imv  1952  19.41v  1956  19.9v  1991  aeveq  2065  sbv  2099  sbequ2  2261  mo4  2570  rspn0  4291  relopabi  5772  lfuhgr3  35355  bj-cbveximdv  36981  bj-spvw  36982  bj-spvew  36983  bj-exextruan  36985  bj-cbvexvv  36987  bj-cbval  36993  bj-cbvexivw  37020  bj-eqs  37023  bj-nnfv  37118  bj-snsetex  37323  bj-snglss  37330  bj-axseprep  37434  bj-axreprepsep  37435  topdifinffinlem  37716  wl-eujustlem1  37966  ac6s6f  38547  ismnushort  44752  fnchoice  45484  ormklocald  47326  natlocalincr  47328