Theorem sbnvOLD

Description: Obsolete version of sbn as of 8-Jul-2023. Substitution is not affected by negation. Version of sbn with a disjoint variable condition, not requiring ax-13 . (Contributed by Wolf Lammen, 18-Jan-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sbnvOLD	$$⊢\left[y/x\right]\neg \phi \leftrightarrow \neg \left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		exanali	$$⊢\exists x\left(x=y\wedge \neg \phi \right)\leftrightarrow \neg \forall x\left(x=y\to \phi \right)$$
2		sb5	$$⊢\left[y/x\right]\neg \phi \leftrightarrow \exists x\left(x=y\wedge \neg \phi \right)$$
3		sb6	$$⊢\left[y/x\right]\phi \leftrightarrow \forall x\left(x=y\to \phi \right)$$
4	3	notbii	$$⊢\neg \left[y/x\right]\phi \leftrightarrow \neg \forall x\left(x=y\to \phi \right)$$
5	1 2 4	3bitr4i	$$⊢\left[y/x\right]\neg \phi \leftrightarrow \neg \left[y/x\right]\phi$$