Theorem sbt

A substitution into a theorem yields a theorem. See sbtALT for a shorter proof requiring more axioms. See chvar and chvarv for versions using implicit substitution. (Contributed by NM, 21-Jan-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Jul-2018.) Revise [df-sb]. (Revised by Steven Nguyen, 6-Jul-2023.) Revise [df-sb] again. (Revised by Wolf Lammen, 4-Feb-2026.)

Hypothesis
sbt.1
\( \vdash \varphi \)
Conclusion
\( \vdash [ t' / x ] \, \varphi \)
Proof
sbt.1
l1
sbtlem _
\( \vdash \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
sbt.1
sbtlem _
2th l1 _
\( \vdash \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \leftrightarrow \forall z \, (z = t' \rightarrow \forall x \, (x = z \rightarrow \varphi)) \)
df-sb _
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
mpbir l1 _