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\in V\to ⦋A/x⦌\left(-B\right)=-⦋A/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		csbov2g	$$⊢A\in V\to ⦋A/x⦌\left(0-B\right)=0-⦋A/x⦌B$$
2		df-neg	$$⊢-B=0-B$$
3	2	csbeq2i	$$⊢⦋A/x⦌\left(-B\right)=⦋A/x⦌\left(0-B\right)$$
4		df-neg	$$⊢-⦋A/x⦌B=0-⦋A/x⦌B$$
5	1 3 4	3eqtr4g	$$⊢A\in V\to ⦋A/x⦌\left(-B\right)=-⦋A/x⦌B$$