Metamath Proof Explorer

Theorem negeq

Description: Equality theorem for negatives. (Contributed by NM, 10-Feb-1995)

Ref Expression
Assertion negeq 
|- ( A = B -> -u A = -u B )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( A = B -> ( 0 - A ) = ( 0 - B ) )
2 df-neg 
 |-  -u A = ( 0 - A )
3 df-neg 
 |-  -u B = ( 0 - B )
4 1 2 3 3eqtr4g 
 |-  ( A = B -> -u A = -u B )