Theorem sbequ

Equality property for substitution, from Tarski's system. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 14-May-1993.) Revise [df-sb]. (Revised by BJ, 30-Dec-2020.)

Conclusion
\( \vdash x' = y' \rightarrow ([ x' / z ] \, \varphi \leftrightarrow [ y' / z ] \, \varphi) \)
Proof
equequ2
imbi1d _
l2
albidv _
\( \vdash x' = y' \rightarrow (\forall u \, (u = x' \rightarrow \forall z \, (z = u \rightarrow \varphi)) \leftrightarrow \forall u \, (u = y' \rightarrow \forall z \, (z = u \rightarrow \varphi))) \)
l3
dfsb
\( \vdash [ x' / z ] \, \varphi \leftrightarrow \forall u \, (u = x' \rightarrow \forall z \, (z = u \rightarrow \varphi)) \)
dfsb
\( \vdash [ y' / z ] \, \varphi \leftrightarrow \forall u \, (u = y' \rightarrow \forall z \, (z = u \rightarrow \varphi)) \)
3bitr4g l2 l3 _