Theorem sb4a
A version of one implication of sb4b that does not require a distinctor
antecedent. Usage of this theorem is discouraged because it depends on
[ax-13]. Use the weaker sb4av when possible. (Contributed by NM,
2-Feb-2007.) Revise [df-sb]. (Revised by Wolf Lammen, 28-Jul-2023.)
(New usage is discouraged.)
Conclusion
\( \vdash [ t / x ] \, \forall t \, \varphi \rightarrow \forall x \, (x = t \rightarrow \varphi) \)
Proof
sbequ2
l1
sps _
\( \vdash \forall x \, x = t \rightarrow [ t / x ] \, \forall t \, \varphi \rightarrow \forall t \, \varphi \)
l2
axc11r
\( \vdash \forall x \, x = t \rightarrow \forall t \, \varphi \rightarrow \forall x \, \varphi \)
ala1
\( \vdash \forall x \, \varphi \rightarrow \forall x \, (x = t \rightarrow \varphi) \)
syl6 l2 _
\( \vdash \forall x \, x = t \rightarrow \forall t \, \varphi \rightarrow \forall x \, (x = t \rightarrow \varphi) \)
l5
syld l1 _
\( \vdash \forall x \, x = t \rightarrow [ t / x ] \, \forall t \, \varphi \rightarrow \forall x \, (x = t \rightarrow \varphi) \)
l6
sb4b
\( \vdash \neg \forall x \, x = t \rightarrow ([ t / x ] \, \forall t \, \varphi \leftrightarrow \forall x \, (x = t \rightarrow \forall t \, \varphi)) \)
sp
imim2i _
alimi _
\( \vdash \forall x \, (x = t \rightarrow \forall t \, \varphi) \rightarrow \forall x \, (x = t \rightarrow \varphi) \)
biimtrdi l6 _
\( \vdash \neg \forall x \, x = t \rightarrow [ t / x ] \, \forall t \, \varphi \rightarrow \forall x \, (x = t \rightarrow \varphi) \)
pm2.61i l5 _