Theorem csbnegg

Description: Move class substitution in and out of the negative of a number. (Contributed by NM, 1-Mar-2008) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Assertion	csbnegg	|- ( A e. V -> [_ A / x ]_ -u B = -u [_ A / x ]_ B )

Proof

Step	Hyp	Ref	Expression
1		csbov2g	|- ( A e. V -> [_ A / x ]_ ( 0 - B ) = ( 0 - [_ A / x ]_ B ) )
2		df-neg	|- -u B = ( 0 - B )
3	2	csbeq2i	|- [_ A / x ]_ -u B = [_ A / x ]_ ( 0 - B )
4		df-neg	|- -u [_ A / x ]_ B = ( 0 - [_ A / x ]_ B )
5	1 3 4	3eqtr4g	|- ( A e. V -> [_ A / x ]_ -u B = -u [_ A / x ]_ B )