Simplify definition [df-sb] by removing its provable hypothesis.
(Contributed by Wolf Lammen, 5-Feb-2026.)
Conclusion
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
Proof
sbjust
\( \vdash \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \leftrightarrow \forall z \, (z = t' \rightarrow \forall x \, (x = z \rightarrow \varphi)) \)