Definition df-neg 8435

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 8433 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 8433	. 2 class -u A
3		cc0 8115	. . 3 class 0
4		cmin 8432	. . 3 class -
5	3, 1, 4	co 6041	. 2 class ( 0 - A )
6	2, 5	wceq 1398	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8454  nfnegd  8457  csbnegg  8459  negcl  8461  neg0  8507  negid  8508  negsub  8509  subneg  8510  negneg  8511  negsubdi  8517  renegcl  8522  mulneg1  8656  ltneg  8724  leneg  8727  ixi  8845  0mnnnnn0  9516  fzshftral  10428  bernneq2  11009  cji  11565  bdtri  11903  m1bits  12624  bitsinv1lem  12625  prmdiv  12910  pcrec  12984  pcid  13000  4sqlem6  13059  4sqlem10  13063  sin0pilem1  15616  cospi  15635  coshalfpip  15657  ptolemy  15659  logbrec  15795  1sgm2ppw  15833  lgslem4  15846  lgseisen  15917  qdiff  16803