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  2286  mo4  2593  rspn0  4307  relopabi  5807  lfuhgr3  29615  bj-cbveximdv  37372  bj-spvw  37373  bj-spvew  37374  bj-exextruan  37376  bj-cbvexvv  37378  bj-cbval  37384  bj-cbvexivw  37411  bj-eqs  37414  bj-nnfv  37509  bj-snsetex  37715  bj-snglss  37722  bj-axseprep  37827  bj-axreprepsep  37828  topdifinffinlem  38109  wl-eujustlem1  38359  ac6s6f  38929  ismnushort  45133  fnchoice  45871  ormklocald  47712