Definition df-neg 8072

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 8070 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 8070	. 2 class -u A
3		cc0 7753	. . 3 class 0
4		cmin 8069	. . 3 class -
5	3, 1, 4	co 5842	. 2 class ( 0 - A )
6	2, 5	wceq 1343	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8091  nfnegd  8094  csbnegg  8096  negcl  8098  neg0  8144  negid  8145  negsub  8146  subneg  8147  negneg  8148  negsubdi  8154  renegcl  8159  mulneg1  8293  ltneg  8360  leneg  8363  ixi  8481  0mnnnnn0  9146  fzshftral  10043  bernneq2  10576  cji  10844  bdtri  11181  prmdiv  12167  pcrec  12240  pcid  12255  4sqlem6  12313  4sqlem10  12317  sin0pilem1  13342  cospi  13361  coshalfpip  13383  ptolemy  13385  logbrec  13518  lgslem4  13544