Theorem sb2
One direction of a simplified definition of substitution. The converse
requires either a disjoint variable condition ( sb6) or a nonfreeness
hypothesis ( sb6f ). Usage of this theorem is discouraged because it
depends on [ax-13]. (Contributed by NM, 13-May-1993.) Revise [df-sb].
(Revised by Wolf Lammen, 26-Jul-2023.) (New usage is discouraged.)
Conclusion
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \rightarrow [ y' / x ] \, \varphi \)
Proof
pm2.27
l1
al2imi _
\( \vdash \forall x \, x = y' \rightarrow \forall x \, (x = y' \rightarrow \varphi) \rightarrow \forall x \, \varphi \)
stdpc4
\( \vdash \forall x \, \varphi \rightarrow [ y' / x ] \, \varphi \)
l3
syl6 l1 _
\( \vdash \forall x \, x = y' \rightarrow \forall x \, (x = y' \rightarrow \varphi) \rightarrow [ y' / x ] \, \varphi \)
sb4b
biimprd _
\( \vdash \neg \forall x \, x = y' \rightarrow \forall x \, (x = y' \rightarrow \varphi) \rightarrow [ y' / x ] \, \varphi \)
pm2.61i l3 _