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	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ - 𝐵 = - ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		csbov2g	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 0 − 𝐵 ) = ( 0 − ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
2		df-neg	⊢ - 𝐵 = ( 0 − 𝐵 )
3	2	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ - 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ ( 0 − 𝐵 )
4		df-neg	⊢ - ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ( 0 − ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
5	1 3 4	3eqtr4g	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ - 𝐵 = - ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )