Theorem ax5e

A rephrasing of [ax-5] using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017.)

Conclusion
\( \vdash \exists x \, \varphi \rightarrow \varphi \)
Proof
l0
ax-5
\( \vdash \neg \varphi \rightarrow \forall x \, \neg \varphi \)
eximal
\( \vdash \exists x \, \varphi \rightarrow \varphi \leftrightarrow \neg \varphi \rightarrow \forall x \, \neg \varphi \)
mpbir l0 _