Theorem equsb1

Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker equsb1v if possible. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)

Conclusion
\( \vdash [ y' / x ] \, x = y' \)
Proof
l0
sb2
\( \vdash \forall x \, (x = y' \rightarrow x = y') \rightarrow [ y' / x ] \, x = y' \)
id
\( \vdash x = y' \rightarrow x = y' \)
mpg l0 _