Definition df-neg 8331

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 8329 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 8329	. 2 class -u A
3		cc0 8010	. . 3 class 0
4		cmin 8328	. . 3 class -
5	3, 1, 4	co 6007	. 2 class ( 0 - A )
6	2, 5	wceq 1395	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8350  nfnegd  8353  csbnegg  8355  negcl  8357  neg0  8403  negid  8404  negsub  8405  subneg  8406  negneg  8407  negsubdi  8413  renegcl  8418  mulneg1  8552  ltneg  8620  leneg  8623  ixi  8741  0mnnnnn0  9412  fzshftral  10316  bernneq2  10895  cji  11429  bdtri  11767  m1bits  12487  bitsinv1lem  12488  prmdiv  12773  pcrec  12847  pcid  12863  4sqlem6  12922  4sqlem10  12926  sin0pilem1  15471  cospi  15490  coshalfpip  15512  ptolemy  15514  logbrec  15650  1sgm2ppw  15685  lgslem4  15698  lgseisen  15769