Theorem sbcni

Description: Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)

	Ref	Expression
Hypotheses	sbcni.1	$$⊢A\in \mathrm{V}$$
	sbcni.2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
Assertion	sbcni	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \psi$$

Proof

Step	Hyp	Ref	Expression
1		sbcni.1	$$⊢A\in \mathrm{V}$$
2		sbcni.2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
3		sbcng	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4	1 3	ax-mp	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
5	4 2	xchbinx	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \psi$$