Theorem sbcni

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

	Ref	Expression
Hypotheses	sbcni.1	⊢ 𝐴 ∈ V
	sbcni.2	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 )
Assertion	sbcni	⊢ ( [ 𝐴 / 𝑥 ] ¬ 𝜑 ↔ ¬ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		sbcni.1	⊢ 𝐴 ∈ V
2		sbcni.2	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 )
3		sbcng	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) )
4	1 3	ax-mp	⊢ ( [ 𝐴 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝐴 / 𝑥 ] 𝜑 )
5	4 2	xchbinx	⊢ ( [ 𝐴 / 𝑥 ] ¬ 𝜑 ↔ ¬ 𝜓 )