Definition df-neg 8193

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 8191 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 8191	. 2 class -u A
3		cc0 7872	. . 3 class 0
4		cmin 8190	. . 3 class -
5	3, 1, 4	co 5918	. 2 class ( 0 - A )
6	2, 5	wceq 1364	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8212  nfnegd  8215  csbnegg  8217  negcl  8219  neg0  8265  negid  8266  negsub  8267  subneg  8268  negneg  8269  negsubdi  8275  renegcl  8280  mulneg1  8414  ltneg  8481  leneg  8484  ixi  8602  0mnnnnn0  9272  fzshftral  10174  bernneq2  10732  cji  11046  bdtri  11383  prmdiv  12373  pcrec  12446  pcid  12462  4sqlem6  12521  4sqlem10  12525  sin0pilem1  14916  cospi  14935  coshalfpip  14957  ptolemy  14959  logbrec  15092  lgslem4  15119  lgseisen  15190