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\in ℂ$$
3		subid	$$⊢0\in ℂ\to 0-0=0$$
4	2 3	ax-mp	$$⊢0-0=0$$
5	1 4	eqtri	$$⊢-0=0$$