sbcng

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

		Ref	Expression
	Assertion	sbcng	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} \neg φ \leftrightarrow \neg \underset{˙}{[} A / x \underset{˙}{]} φ)$

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

Metamath Proof Explorer