Theorem sbequ2
An equality theorem for substitution. (Contributed by NM, 16-May-1993.)
Revise [df-sb]. (Revised by BJ, 22-Dec-2020.) (Proof shortened by
Wolf Lammen, 3-Feb-2024.)
Conclusion
\( \vdash x = t' \rightarrow [ t' / x ] \, \varphi \rightarrow \varphi \)
Proof
dfsb
l1
biimpi _
\( \vdash [ t' / x ] \, \varphi \rightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
l2
equvinva
\( \vdash x = t' \rightarrow \exists y \, (x = y \wedge t' = y) \)
l3
equcomi
sp
imim12i l3 _
impcomd _
aleximi _
\( \vdash \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \rightarrow \exists y \, (x = y \wedge t' = y) \rightarrow \exists y \, \varphi \)
l8
syl2im l1 l2 _
\( \vdash [ t' / x ] \, \varphi \rightarrow x = t' \rightarrow \exists y \, \varphi \)
ax5e
\( \vdash \exists y \, \varphi \rightarrow \varphi \)
syl6com l8 _