Theorem equsb2

Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on [ax-13]. Check out equsb1v for a version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)

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