Theorem sbn

Description: 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)

	Ref	Expression
Assertion	sbn	$$⊢\left[t/x\right]\neg \phi \leftrightarrow \neg \left[t/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		df-sb	$$⊢\left[t/x\right]\neg \phi \leftrightarrow \forall y\left(y=t\to \forall x\left(x=y\to \neg \phi \right)\right)$$
2		alinexa	$$⊢\forall x\left(x=y\to \neg \phi \right)\leftrightarrow \neg \exists x\left(x=y\wedge \phi \right)$$
3	2	imbi2i	$$⊢\left(y=t\to \forall x\left(x=y\to \neg \phi \right)\right)\leftrightarrow \left(y=t\to \neg \exists x\left(x=y\wedge \phi \right)\right)$$
4	3	albii	$$⊢\forall y\left(y=t\to \forall x\left(x=y\to \neg \phi \right)\right)\leftrightarrow \forall y\left(y=t\to \neg \exists x\left(x=y\wedge \phi \right)\right)$$
5		alinexa	$$⊢\forall y\left(y=t\to \neg \exists x\left(x=y\wedge \phi \right)\right)\leftrightarrow \neg \exists y\left(y=t\wedge \exists x\left(x=y\wedge \phi \right)\right)$$
6		dfsb7	$$⊢\left[t/x\right]\phi \leftrightarrow \exists y\left(y=t\wedge \exists x\left(x=y\wedge \phi \right)\right)$$
7	5 6	xchbinxr	$$⊢\forall y\left(y=t\to \neg \exists x\left(x=y\wedge \phi \right)\right)\leftrightarrow \neg \left[t/x\right]\phi$$
8	1 4 7	3bitri	$$⊢\left[t/x\right]\neg \phi \leftrightarrow \neg \left[t/x\right]\phi$$