Definition df-neg 8501

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 8499 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 8499	. 2 class -u A
3		cc0 8179	. . 3 class 0
4		cmin 8498	. . 3 class -
5	3, 1, 4	co 6085	. 2 class ( 0 - A )
6	2, 5	wceq 1402	1 wff -u A = ( 0 - A )

This definition is used by:  negeq  8520  nfnegd  8523  csbnegg  8525  negcl  8527  neg0  8573  negid  8574  negsub  8575  subneg  8576  negneg  8577  negsubdi  8583  renegcl  8588  addeq0  8704  mulneg1  8723  ltneg  8791  leneg  8794  ixi  8913  0mnnnnn0  9599  fz00m1  10461  fzshftral  10525  bernneq2  11112  cji  11682  bdtri  12022  m1bits  12743  bitsinv1lem  12744  prmdiv  13033  pcrec  13107  pcid  13123  4sqlem6  13182  4sqlem10  13186  ballotfilem1c  13300  sin0pilem1  15932  cospi  15951  coshalfpip  15973  ptolemy  15975  logbrec  16115  1sgm2ppw  16190  lgslem4  16220  lgseisen  16291  qdiff  17196