Definition df-neg 8162

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 8160 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 8160	. 2 class -u A
3		cc0 7842	. . 3 class 0
4		cmin 8159	. . 3 class -
5	3, 1, 4	co 5897	. 2 class ( 0 - A )
6	2, 5	wceq 1364	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8181  nfnegd  8184  csbnegg  8186  negcl  8188  neg0  8234  negid  8235  negsub  8236  subneg  8237  negneg  8238  negsubdi  8244  renegcl  8249  mulneg1  8383  ltneg  8450  leneg  8453  ixi  8571  0mnnnnn0  9239  fzshftral  10140  bernneq2  10676  cji  10946  bdtri  11283  prmdiv  12270  pcrec  12343  pcid  12359  4sqlem6  12418  4sqlem10  12422  sin0pilem1  14679  cospi  14698  coshalfpip  14720  ptolemy  14722  logbrec  14855  lgslem4  14882