Theorem ax5e 1945

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  ax5ea  1946  exlimiv  1963  exlimdv  1966  19.21v  1972  19.23v  1975  19.36imv  1978  19.41v  1982  19.9v  2017  aeveq  2091  sbv  2125  sbequ2  2288  mo4  2597  rspn0  4314  relopabi  5814  lfuhgr3  35633  bj-cbveximdv  37297  bj-spvw  37298  bj-spvew  37299  bj-exextruan  37301  bj-cbvexvv  37303  bj-cbval  37309  bj-cbvexivw  37336  bj-eqs  37339  bj-nnfv  37434  bj-snsetex  37640  bj-snglss  37647  bj-axseprep  37752  bj-axreprepsep  37753  topdifinffinlem  38034  wl-eujustlem1  38284  ac6s6f  38863  ismnushort  45052  fnchoice  45790  ormklocald  47631  natlocalincr  47633