Definition df-neg 7807

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 7805 for a discussion of this. (Contributed by NM, 10-Feb-1995.)

Assertion

Ref	Expression
df-neg	|- -u A = ( 0 - A )

Detailed syntax breakdown of Definition df-neg

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cneg 7805	. 2 class -u A
3		cc0 7500	. . 3 class 0
4		cmin 7804	. . 3 class -
5	3, 1, 4	co 5706	. 2 class ( 0 - A )
6	2, 5	wceq 1299	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  7826  nfnegd  7829  csbnegg  7831  negcl  7833  neg0  7879  negid  7880  negsub  7881  subneg  7882  negneg  7883  negsubdi  7889  renegcl  7894  mulneg1  8024  ltneg  8091  leneg  8094  ixi  8211  0mnnnnn0  8861  fzshftral  9729  bernneq2  10254  cji  10515  bdtri  10850