Theorem sbcng

Description: Move negation in and out of class substitution. (Contributed by NM, 16-Jan-2004)

	Ref	Expression
Assertion	sbcng	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		dfsbcq2	$$⊢y=A\to \left(\left[y/x\right]\neg \phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \right)$$
2		dfsbcq2	$$⊢y=A\to \left(\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
3	2	notbid	$$⊢y=A\to \left(\neg \left[y/x\right]\phi \leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4		sbn	$$⊢\left[y/x\right]\neg \phi \leftrightarrow \neg \left[y/x\right]\phi$$
5	1 3 4	vtoclbg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$