Theorem hbae
All variables are effectively bound in an identical variable specifier.
Usage of this theorem is discouraged because it depends on [ax-13]. Use
the weaker hbaev when possible. (Contributed by NM, 13-May-1993.)
(Proof shortened by Wolf Lammen, 21-Apr-2018.)
(New usage is discouraged.)
Conclusion
\( \vdash \forall x \, x = y \rightarrow \forall z \, \forall x \, x = y \)
Proof
l0
sp
\( \vdash \forall x \, x = y \rightarrow x = y \)
axc9
\( \vdash \neg \forall z \, z = x \rightarrow \neg \forall z \, z = y \rightarrow x = y \rightarrow \forall z \, x = y \)
l2
syl7 l0 _
\( \vdash \neg \forall z \, z = x \rightarrow \neg \forall z \, z = y \rightarrow \forall x \, x = y \rightarrow \forall z \, x = y \)
l3
axc11r
\( \vdash \forall z \, z = x \rightarrow \forall x \, x = y \rightarrow \forall z \, x = y \)
axc11
l5
pm2.43i _
\( \vdash \forall x \, x = y \rightarrow \forall y \, x = y \)
axc11r
\( \vdash \forall z \, z = y \rightarrow \forall y \, x = y \rightarrow \forall z \, x = y \)
syl5 l5 _
\( \vdash \forall z \, z = y \rightarrow \forall x \, x = y \rightarrow \forall z \, x = y \)
pm2.61ii l2 l3 _
l9
axc4i _
\( \vdash \forall x \, x = y \rightarrow \forall x \, \forall z \, x = y \)
ax-11
\( \vdash \forall x \, \forall z \, x = y \rightarrow \forall z \, \forall x \, x = y \)
syl l9 _