Definition df-neg 8500

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 8498 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 8498	. 2 class -u A
3		cc0 8179	. . 3 class 0
4		cmin 8497	. . 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  8519  nfnegd  8522  csbnegg  8524  negcl  8526  neg0  8572  negid  8573  negsub  8574  subneg  8575  negneg  8576  negsubdi  8582  renegcl  8587  addeq0  8703  mulneg1  8722  ltneg  8790  leneg  8793  ixi  8911  0mnnnnn0  9595  fz00m1  10451  fzshftral  10515  bernneq2  11099  cji  11668  bdtri  12006  m1bits  12727  bitsinv1lem  12728  prmdiv  13013  pcrec  13087  pcid  13103  4sqlem6  13162  4sqlem10  13166  ballotfilem1c  13251  sin0pilem1  15882  cospi  15901  coshalfpip  15923  ptolemy  15925  logbrec  16062  1sgm2ppw  16109  lgslem4  16122  lgseisen  16193  qdiff  17098