Definition df-neg 8195

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 8193 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 8193	. 2 class -u A
3		cc0 7874	. . 3 class 0
4		cmin 8192	. . 3 class -
5	3, 1, 4	co 5919	. 2 class ( 0 - A )
6	2, 5	wceq 1364	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8214  nfnegd  8217  csbnegg  8219  negcl  8221  neg0  8267  negid  8268  negsub  8269  subneg  8270  negneg  8271  negsubdi  8277  renegcl  8282  mulneg1  8416  ltneg  8483  leneg  8486  ixi  8604  0mnnnnn0  9275  fzshftral  10177  bernneq2  10735  cji  11049  bdtri  11386  prmdiv  12376  pcrec  12449  pcid  12465  4sqlem6  12524  4sqlem10  12528  sin0pilem1  14957  cospi  14976  coshalfpip  14998  ptolemy  15000  logbrec  15133  lgslem4  15160  lgseisen  15231