Theorem stdpc4

The specialization axiom of standard predicate calculus. It states that if a statement \( \varphi \) holds for all \( x \), then it also holds for the specific case of \( t' \) (properly) substituted for \( x \). Translated to traditional notation, it can be read: " A. x ph ( x ) -> ph ( t ), provided that \( t' \) is free for \( x \) in ph ( x ) ". Axiom 4 of [Mendelson] p. 69. See also [spsbc] and [rspsbc]. (Contributed by NM, 14-May-1993.) Revise [df-sb]. (Revised by BJ, 22-Dec-2020.)

Conclusion
\( \vdash \forall x \, \varphi \rightarrow [ t' / x ] \, \varphi \)
Proof
ala1
a1d _
l2
alrimiv _
\( \vdash \forall x \, \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)) \)
sylibr l2 _