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 e. _V
	sbcni.2	|- ( [. A / x ]. ph <-> ps )
Assertion	sbcni	|- ( [. A / x ]. -. ph <-> -. ps )

Proof

Step	Hyp	Ref	Expression
1		sbcni.1	|- A e. _V
2		sbcni.2	|- ( [. A / x ]. ph <-> ps )
3		sbcng	|- ( A e. _V -> ( [. A / x ]. -. ph <-> -. [. A / x ]. ph ) )
4	1 3	ax-mp	|- ( [. A / x ]. -. ph <-> -. [. A / x ]. ph )
5	4 2	xchbinx	|- ( [. A / x ]. -. ph <-> -. ps )