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  10468  fzshftral  10532  bernneq2  11120  cji  11690  bdtri  12031  m1bits  12752  bitsinv1lem  12753  prmdiv  13042  pcrec  13116  pcid  13132  4sqlem6  13191  4sqlem10  13195  ballotfilem1c  13309  sin0pilem1  16008  cospi  16027  coshalfpip  16049  ptolemy  16051  logbrec  16196  1sgm2ppw  16289  lgslem4  16327  lgseisen  16398  qdiff  17305