Theorem sb1
One direction of a simplified definition of substitution. The converse
requires either a disjoint variable condition ( sb5) or a nonfreeness
hypothesis ( sb5f ). Usage of this theorem is discouraged because it
depends on [ax-13]. Use the weaker sb1v when possible. (Contributed
by NM, 13-May-1993.) Revise [df-sb]. (Revised by Wolf Lammen,
21-Feb-2024.) (New usage is discouraged.)
Conclusion
\( \vdash [ y' / x ] \, \varphi \rightarrow \exists x \, (x = y' \wedge \varphi) \)
Proof
l0
spsbe
\( \vdash [ y' / x ] \, \varphi \rightarrow \exists x \, \varphi \)
pm3.2
aleximi _
\( \vdash \forall x \, x = y' \rightarrow \exists x \, \varphi \rightarrow \exists x \, (x = y' \wedge \varphi) \)
l3
syl5 l0 _
\( \vdash \forall x \, x = y' \rightarrow [ y' / x ] \, \varphi \rightarrow \exists x \, (x = y' \wedge \varphi) \)
sb3b
biimpd _
\( \vdash \neg \forall x \, x = y' \rightarrow [ y' / x ] \, \varphi \rightarrow \exists x \, (x = y' \wedge \varphi) \)
pm2.61i l3 _