Theorem neg0

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

	Ref	Expression
Assertion	neg0	⊢ - 0 = 0

Proof

Step	Hyp	Ref	Expression
1		df-neg	⊢ - 0 = ( 0 − 0 )
2		0cn	⊢ 0 ∈ ℂ
3		subid	⊢ ( 0 ∈ ℂ → ( 0 − 0 ) = 0 )
4	2 3	ax-mp	⊢ ( 0 − 0 ) = 0
5	1 4	eqtri	⊢ - 0 = 0