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

Metamath Proof Explorer

Definition df-neg

Description: Define the negative of a number (unary minus). We use different symbols for unary minus ( -u ) and subtraction ( - ) to prevent syntax ambiguity. See cneg for a discussion of this. (Contributed by NM, 10-Feb-1995)

		Ref	Expression
	Assertion	df-neg	⊢ - 𝐴 = ( 0 − 𝐴 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	cneg	⊢ - 𝐴
2		cc0	⊢ 0
3		cmin	⊢ −
4	2 0 3	co	⊢ ( 0 − 𝐴 )
5	1 4	wceq	⊢ - 𝐴 = ( 0 − 𝐴 )