Theorem hbe1w

Weak version of hbe1. See comments for ax10w. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.)

Hypothesis
hbn1w.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
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 \)
hbn1w.1
notbid _
\( \vdash x = y \rightarrow (\neg \varphi \leftrightarrow \neg \psi) \)
hbn1w _
\( \vdash \neg \forall x \, \neg \varphi \rightarrow \forall x \, \neg \forall x \, \neg \varphi \)
hbxfrbi l0 _