Definition df-neg 8125

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 8123 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 8123	. 2 class -u A
3		cc0 7806	. . 3 class 0
4		cmin 8122	. . 3 class -
5	3, 1, 4	co 5870	. 2 class ( 0 - A )
6	2, 5	wceq 1353	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8144  nfnegd  8147  csbnegg  8149  negcl  8151  neg0  8197  negid  8198  negsub  8199  subneg  8200  negneg  8201  negsubdi  8207  renegcl  8212  mulneg1  8346  ltneg  8413  leneg  8416  ixi  8534  0mnnnnn0  9202  fzshftral  10101  bernneq2  10634  cji  10902  bdtri  11239  prmdiv  12225  pcrec  12298  pcid  12313  4sqlem6  12371  4sqlem10  12375  sin0pilem1  13984  cospi  14003  coshalfpip  14025  ptolemy  14027  logbrec  14160  lgslem4  14186