Definition df-neg 8080

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 8078 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 8078	. 2 class -u A
3		cc0 7761	. . 3 class 0
4		cmin 8077	. . 3 class -
5	3, 1, 4	co 5850	. 2 class ( 0 - A )
6	2, 5	wceq 1348	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8099  nfnegd  8102  csbnegg  8104  negcl  8106  neg0  8152  negid  8153  negsub  8154  subneg  8155  negneg  8156  negsubdi  8162  renegcl  8167  mulneg1  8301  ltneg  8368  leneg  8371  ixi  8489  0mnnnnn0  9154  fzshftral  10051  bernneq2  10584  cji  10853  bdtri  11190  prmdiv  12176  pcrec  12249  pcid  12264  4sqlem6  12322  4sqlem10  12326  sin0pilem1  13455  cospi  13474  coshalfpip  13496  ptolemy  13498  logbrec  13631  lgslem4  13657