Theorem sbequ12a

An equality theorem for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Jun-2019.)

Conclusion
\( \vdash x = y \rightarrow ([ y / x ] \, \varphi \leftrightarrow [ x / y ] \, \varphi) \)
Proof
l0
sbequ12r
\( \vdash x = y \rightarrow ([ x / y ] \, \varphi \leftrightarrow \varphi) \)
sbequ12
\( \vdash x = y \rightarrow (\varphi \leftrightarrow [ y / x ] \, \varphi) \)
bitr2d l0 _