Definition df-neg 8507

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 8505 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 8505	. 2 class -u A
3		cc0 8185	. . 3 class 0
4		cmin 8504	. . 3 class -
5	3, 1, 4	co 6088	. 2 class ( 0 - A )
6	2, 5	wceq 1402	1 wff -u A = ( 0 - A )

This definition is used by:  negeq  8526  nfnegd  8529  csbnegg  8531  negcl  8533  neg0  8579  negid  8580  negsub  8581  subneg  8582  negneg  8583  negsubdi  8589  renegcl  8594  addeq0  8710  mulneg1  8729  ltneg  8797  leneg  8800  ixi  8919  0mnnnnn0  9606  fz00m1  10467  fzshftral  10531  bernneq2  11119  cji  11689  bdtri  12030  m1bits  12751  bitsinv1lem  12752  prmdiv  13041  pcrec  13115  pcid  13131  4sqlem6  13190  4sqlem10  13194  ballotfilem1c  13308  sin0pilem1  16025  cospi  16044  coshalfpip  16066  ptolemy  16068  logbrec  16213  1sgm2ppw  16306  lgslem4  16344  lgseisen  16415  qdiff  17322