Theorem hbnaes

Rule that applies hbnae to antecedent. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 15-May-1993.) (New usage is discouraged.)

Hypothesis
hbnaes.1
\( \vdash \forall z \, \neg \forall x \, x = y \rightarrow \varphi \)
Conclusion
\( \vdash \neg \forall x \, x = y \rightarrow \varphi \)
Proof
l0
hbnae
\( \vdash \neg \forall x \, x = y \rightarrow \forall z \, \neg \forall x \, x = y \)
hbnaes.1
\( \vdash \forall z \, \neg \forall x \, x = y \rightarrow \varphi \)
syl l0 _