Theorem sb4b
Simplified definition of substitution when variables are distinct.
Version of sb6 with a distinctor antecedent. Usage of this theorem is
discouraged because it depends on [ax-13]. (Contributed by NM,
27-May-1997.) Revise [df-sb]. (Revised by Wolf Lammen, 21-Feb-2024.)
(New usage is discouraged.)
Conclusion
\( \vdash \neg \forall x \, x = t' \rightarrow ([ t' / x ] \, \varphi \leftrightarrow \forall x \, (x = t' \rightarrow \varphi)) \)
Proof
l0
nfna1
nfeqf2
l2
nfan1 l0 _
equequ2
imbi1d _
adantl _
albid l2 _
pm5.74da _
l8
albidv _
\( \vdash \neg \forall x \, x = t' \rightarrow (\forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \leftrightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = t' \rightarrow \varphi))) \)
l9
dfsb
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
ax6ev
l11
a1bi _
\( \vdash \forall x \, (x = t' \rightarrow \varphi) \leftrightarrow \exists y \, y = t' \rightarrow \forall x \, (x = t' \rightarrow \varphi) \)
19.23v
\( \vdash \forall y \, (y = t' \rightarrow \forall x \, (x = t' \rightarrow \varphi)) \leftrightarrow \exists y \, y = t' \rightarrow \forall x \, (x = t' \rightarrow \varphi) \)
bitr4i l11 _
\( \vdash \forall x \, (x = t' \rightarrow \varphi) \leftrightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = t' \rightarrow \varphi)) \)
3bitr4g l8 l9 _