Definition df-neg 8248

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 8246 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 8246	. 2 class -u A
3		cc0 7927	. . 3 class 0
4		cmin 8245	. . 3 class -
5	3, 1, 4	co 5946	. 2 class ( 0 - A )
6	2, 5	wceq 1373	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8267  nfnegd  8270  csbnegg  8272  negcl  8274  neg0  8320  negid  8321  negsub  8322  subneg  8323  negneg  8324  negsubdi  8330  renegcl  8335  mulneg1  8469  ltneg  8537  leneg  8540  ixi  8658  0mnnnnn0  9329  fzshftral  10232  bernneq2  10808  cji  11246  bdtri  11584  m1bits  12304  bitsinv1lem  12305  prmdiv  12590  pcrec  12664  pcid  12680  4sqlem6  12739  4sqlem10  12743  sin0pilem1  15286  cospi  15305  coshalfpip  15327  ptolemy  15329  logbrec  15465  1sgm2ppw  15500  lgslem4  15513  lgseisen  15584