Theorem axie1

The setvar \( x \) is not free in \( \exists x \, \varphi \) (intuitionistic logic axiom ax-ie1). (Contributed by Jim Kingdon, 31-Dec-2017.) (New usage is discouraged.)

Conclusion
\( \vdash \exists x \, \varphi \rightarrow \forall x \, \exists x \, \varphi \)
Proof
hbe1