Definition df-neg 8133

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 8131 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 8131	. 2 class -u A
3		cc0 7813	. . 3 class 0
4		cmin 8130	. . 3 class -
5	3, 1, 4	co 5877	. 2 class ( 0 - A )
6	2, 5	wceq 1353	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8152  nfnegd  8155  csbnegg  8157  negcl  8159  neg0  8205  negid  8206  negsub  8207  subneg  8208  negneg  8209  negsubdi  8215  renegcl  8220  mulneg1  8354  ltneg  8421  leneg  8424  ixi  8542  0mnnnnn0  9210  fzshftral  10110  bernneq2  10644  cji  10913  bdtri  11250  prmdiv  12237  pcrec  12310  pcid  12325  4sqlem6  12383  4sqlem10  12387  sin0pilem1  14241  cospi  14260  coshalfpip  14282  ptolemy  14284  logbrec  14417  lgslem4  14443