Definition df-neg 8200

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 8198 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 8198	. 2 class -u A
3		cc0 7879	. . 3 class 0
4		cmin 8197	. . 3 class -
5	3, 1, 4	co 5922	. 2 class ( 0 - A )
6	2, 5	wceq 1364	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8219  nfnegd  8222  csbnegg  8224  negcl  8226  neg0  8272  negid  8273  negsub  8274  subneg  8275  negneg  8276  negsubdi  8282  renegcl  8287  mulneg1  8421  ltneg  8489  leneg  8492  ixi  8610  0mnnnnn0  9281  fzshftral  10183  bernneq2  10753  cji  11067  bdtri  11405  prmdiv  12403  pcrec  12477  pcid  12493  4sqlem6  12552  4sqlem10  12556  sin0pilem1  15017  cospi  15036  coshalfpip  15058  ptolemy  15060  logbrec  15196  1sgm2ppw  15231  lgslem4  15244  lgseisen  15315