This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbcn1

Description: Move negation in and out of class substitution. One direction of sbcng that holds for proper classes. (Contributed by NM, 17-Aug-2018)

		Ref	Expression
	Assertion	sbcn1	$⊢ \underset{˙}{[} A / x \underset{˙}{]} \neg φ \to \neg \underset{˙}{[} A / x \underset{˙}{]} φ$

Proof

Step	Hyp	Ref	Expression
1		sbcex	$⊢ \underset{˙}{[} A / x \underset{˙}{]} \neg φ \to A \in V$
2		sbcng	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} \neg φ \leftrightarrow \neg \underset{˙}{[} A / x \underset{˙}{]} φ)$
3	2	biimpd	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} \neg φ \to \neg \underset{˙}{[} A / x \underset{˙}{]} φ)$
4	1 3	mpcom	$⊢ \underset{˙}{[} A / x \underset{˙}{]} \neg φ \to \neg \underset{˙}{[} A / x \underset{˙}{]} φ$