Theorem xneg0

Description: The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xneg0	$$⊢-0=0$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		rexneg	$$⊢0\in ℝ\to -0=-0$$
3	1 2	ax-mp	$$⊢-0=-0$$
4		neg0	$$⊢-0=0$$
5	3 4	eqtri	$$⊢-0=0$$