Theorem hbnae

All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker hbnaev when possible. (Contributed by NM, 13-May-1993.) (New usage is discouraged.)

Conclusion
\( \vdash \neg \forall x \, x = y \rightarrow \forall z \, \neg \forall x \, x = y \)
Proof
hbae
hbn _