Theorem ax5ea

If a formula holds for some value of a variable not occurring in it, then it holds for all values of that variable. (Contributed by BJ, 28-Dec-2020.)

Conclusion
\( \vdash \exists x \, \varphi \rightarrow \forall x \, \varphi \)
Proof
l0
ax5e
\( \vdash \exists x \, \varphi \rightarrow \varphi \)
ax-5
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
syl l0 _