Metamath Proof Explorer

Theorem neg0

Description: Minus 0 equals 0. (Contributed by NM, 17-Jan-1997)

Ref Expression
Assertion neg0 
|- -u 0 = 0

Proof

Step Hyp Ref Expression
1 df-neg 
 |-  -u 0 = ( 0 - 0 )
2 0cn 
 |-  0 e. CC
3 subid 
 |-  ( 0 e. CC -> ( 0 - 0 ) = 0 )
4 2 3 ax-mp 
 |-  ( 0 - 0 ) = 0
5 1 4 eqtri 
 |-  -u 0 = 0