Definition df-neg 8093

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 8091 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 8091	. 2 class -u A
3		cc0 7774	. . 3 class 0
4		cmin 8090	. . 3 class -
5	3, 1, 4	co 5853	. 2 class ( 0 - A )
6	2, 5	wceq 1348	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8112  nfnegd  8115  csbnegg  8117  negcl  8119  neg0  8165  negid  8166  negsub  8167  subneg  8168  negneg  8169  negsubdi  8175  renegcl  8180  mulneg1  8314  ltneg  8381  leneg  8384  ixi  8502  0mnnnnn0  9167  fzshftral  10064  bernneq2  10597  cji  10866  bdtri  11203  prmdiv  12189  pcrec  12262  pcid  12277  4sqlem6  12335  4sqlem10  12339  sin0pilem1  13496  cospi  13515  coshalfpip  13537  ptolemy  13539  logbrec  13672  lgslem4  13698