Theorem sbequ1

An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise [df-sb]. (Revised by BJ, 22-Dec-2020.)

Conclusion
\( \vdash x = t' \rightarrow \varphi \rightarrow [ t' / x ] \, \varphi \)
Proof
l0
equeucl
\( \vdash x = t' \rightarrow y = t' \rightarrow x = y \)
ax12v
\( \vdash x = y \rightarrow \varphi \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
syl6 l0 _
com23 _
l4
alrimdv _
\( \vdash x = t' \rightarrow \varphi \rightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
dfsb
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
imbitrrdi l4 _