Definition df-neg 8356

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 8354 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 8354	. 2 class -u A
3		cc0 8035	. . 3 class 0
4		cmin 8353	. . 3 class -
5	3, 1, 4	co 6021	. 2 class ( 0 - A )
6	2, 5	wceq 1397	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8375  nfnegd  8378  csbnegg  8380  negcl  8382  neg0  8428  negid  8429  negsub  8430  subneg  8431  negneg  8432  negsubdi  8438  renegcl  8443  mulneg1  8577  ltneg  8645  leneg  8648  ixi  8766  0mnnnnn0  9437  fzshftral  10346  bernneq2  10927  cji  11483  bdtri  11821  m1bits  12542  bitsinv1lem  12543  prmdiv  12828  pcrec  12902  pcid  12918  4sqlem6  12977  4sqlem10  12981  sin0pilem1  15532  cospi  15551  coshalfpip  15573  ptolemy  15575  logbrec  15711  1sgm2ppw  15746  lgslem4  15759  lgseisen  15830  qdiff  16712