Theorem sbjust

Justification theorem for [df-sb] proved from Tarski's FOL axiom schemes. (Contributed by BJ, 22-Jan-2023.)

Conclusion
\( \vdash \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \leftrightarrow \forall z \, (z = t' \rightarrow \forall x \, (x = z \rightarrow \varphi)) \)
Proof
l0
equequ1
equequ2
imbi1d _
albidv _
imbi12d l0 _
cbvalvw _