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	$$⊢-A=0-A$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	cneg	$$class\left(-A\right)$$
2		cc0	$$class0$$
3		cmin	$$class-$$
4	2 0 3	co	$$class\left(0-A\right)$$
5	1 4	wceq	$$wff-A=0-A$$