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  2285  mo4  2592  rspn0  4304  relopabi  5800  lfuhgr3  29710  bj-cbveximdv  37503  bj-spvw  37504  bj-spvew  37505  bj-exextruan  37507  bj-cbvexvv  37509  bj-cbval  37515  bj-cbvexivw  37542  bj-eqs  37545  bj-nnfv  37640  bj-snsetex  37846  bj-snglss  37853  bj-axseprep  37958  bj-axreprepsep  37959  topdifinffinlem  38238  wl-eujustlem1  38488  ac6s6f  39073  ismnushort  45244  fnchoice  45989  ormklocald  47830