Theorem sb2ae

In the case of two successive substitutions for two always equal variables, the second substitution has no effect. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by BJ and WL, 9-Aug-2023.) (New usage is discouraged.)

Conclusion
\( \vdash \forall x \, x = y \rightarrow ([ u' / x ] \, [ v' / y ] \, \varphi \leftrightarrow [ v' / y ] \, \varphi) \)
Proof
l0
drsb1
\( \vdash \forall x \, x = y \rightarrow ([ u' / x ] \, [ v' / y ] \, \varphi \leftrightarrow [ u' / y ] \, [ v' / y ] \, \varphi) \)
nfs1v
sbf _
\( \vdash [ u' / y ] \, [ v' / y ] \, \varphi \leftrightarrow [ v' / y ] \, \varphi \)
bitrdi l0 _