Theorem hbe1

The setvar \( x \) is not free in \( \exists x \, \varphi \). Corresponds to the axiom (5) of modal logic (see also modal5 ). (Contributed by NM, 24-Jan-1993.)

Conclusion
\( \vdash \exists x \, \varphi \rightarrow \forall x \, \exists x \, \varphi \)
Proof
l0
df-ex
\( \vdash \exists x \, \varphi \leftrightarrow \neg \forall x \, \neg \varphi \)
hbn1
\( \vdash \neg \forall x \, \neg \varphi \rightarrow \forall x \, \neg \forall x \, \neg \varphi \)
hbxfrbi l0 _