This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem neg0

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

		Ref	Expression
	Assertion	neg0	$⊢ - 0 = 0$

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$