Definition df-neg 8353

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 8351 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 8351	. 2 class -u A
3		cc0 8032	. . 3 class 0
4		cmin 8350	. . 3 class -
5	3, 1, 4	co 6018	. 2 class ( 0 - A )
6	2, 5	wceq 1397	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8372  nfnegd  8375  csbnegg  8377  negcl  8379  neg0  8425  negid  8426  negsub  8427  subneg  8428  negneg  8429  negsubdi  8435  renegcl  8440  mulneg1  8574  ltneg  8642  leneg  8645  ixi  8763  0mnnnnn0  9434  fzshftral  10343  bernneq2  10923  cji  11463  bdtri  11801  m1bits  12522  bitsinv1lem  12523  prmdiv  12808  pcrec  12882  pcid  12898  4sqlem6  12957  4sqlem10  12961  sin0pilem1  15507  cospi  15526  coshalfpip  15548  ptolemy  15550  logbrec  15686  1sgm2ppw  15721  lgslem4  15734  lgseisen  15805