Theorem sbn
Negation inside and outside of substitution are equivalent.
(Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen,
30-Apr-2018.) Revise [df-sb]. (Revised by BJ, 25-Dec-2020.)
Conclusion
\( \vdash [ t' / x ] \, (\neg \varphi) \leftrightarrow \neg [ t' / x ] \, \varphi \)
Proof
l0
dfsb
\( \vdash [ t' / x ] \, (\neg \varphi) \leftrightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \neg \varphi)) \)
alinexa
imbi2i _
l3
albii _
\( \vdash \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \neg \varphi)) \leftrightarrow \forall y \, (y = t' \rightarrow \neg \exists x \, (x = y \wedge \varphi)) \)
l4
alinexa
\( \vdash \forall y \, (y = t' \rightarrow \neg \exists x \, (x = y \wedge \varphi)) \leftrightarrow \neg \exists y \, (y = t' \wedge \exists x \, (x = y \wedge \varphi)) \)
dfsb7
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \exists y \, (y = t' \wedge \exists x \, (x = y \wedge \varphi)) \)
xchbinxr l4 _
\( \vdash \forall y \, (y = t' \rightarrow \neg \exists x \, (x = y \wedge \varphi)) \leftrightarrow \neg [ t' / x ] \, \varphi \)
3bitri l0 l3 _