Definition df-neg 8446

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 8444 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 8444	. 2 class -u A
3		cc0 8126	. . 3 class 0
4		cmin 8443	. . 3 class -
5	3, 1, 4	co 6049	. 2 class ( 0 - A )
6	2, 5	wceq 1398	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8465  nfnegd  8468  csbnegg  8470  negcl  8472  neg0  8518  negid  8519  negsub  8520  subneg  8521  negneg  8522  negsubdi  8528  renegcl  8533  mulneg1  8667  ltneg  8735  leneg  8738  ixi  8856  0mnnnnn0  9527  fzshftral  10441  bernneq2  11022  cji  11583  bdtri  11921  m1bits  12642  bitsinv1lem  12643  prmdiv  12928  pcrec  13002  pcid  13018  4sqlem6  13077  4sqlem10  13081  sin0pilem1  15638  cospi  15657  coshalfpip  15679  ptolemy  15681  logbrec  15817  1sgm2ppw  15855  lgslem4  15868  lgseisen  15939  qdiff  16825