Theorem sbequ5

Substitution does not change an identical variable specifier. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 15-May-1993.) (New usage is discouraged.)

Conclusion
\( \vdash [ w' / z ] \, \forall x \, x = y \leftrightarrow \forall x \, x = y \)
Proof
nfae
sbf _