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	|- -u A = ( 0 - A )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	cneg	|- -u A
2		cc0	|- 0
3		cmin	|- -
4	2 0 3	co	|- ( 0 - A )
5	1 4	wceq	|- -u A = ( 0 - A )