Definition df-neg 8320

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 8318 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 8318	. 2 class -u A
3		cc0 7999	. . 3 class 0
4		cmin 8317	. . 3 class -
5	3, 1, 4	co 6001	. 2 class ( 0 - A )
6	2, 5	wceq 1395	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8339  nfnegd  8342  csbnegg  8344  negcl  8346  neg0  8392  negid  8393  negsub  8394  subneg  8395  negneg  8396  negsubdi  8402  renegcl  8407  mulneg1  8541  ltneg  8609  leneg  8612  ixi  8730  0mnnnnn0  9401  fzshftral  10304  bernneq2  10883  cji  11413  bdtri  11751  m1bits  12471  bitsinv1lem  12472  prmdiv  12757  pcrec  12831  pcid  12847  4sqlem6  12906  4sqlem10  12910  sin0pilem1  15455  cospi  15474  coshalfpip  15496  ptolemy  15498  logbrec  15634  1sgm2ppw  15669  lgslem4  15682  lgseisen  15753