Definition df-neg 8130

Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction (−) to prevent syntax ambiguity. See cneg 8128 for a discussion of this. (Contributed by NM, 10-Feb-1995.)

Assertion

Ref	Expression
df-neg	⊢ -𝐴 = (0 − 𝐴)

Detailed syntax breakdown of Definition df-neg

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	cneg 8128	. 2 class -𝐴
3		cc0 7810	. . 3 class 0
4		cmin 8127	. . 3 class −
5	3, 1, 4	co 5874	. 2 class (0 − 𝐴)
6	2, 5	wceq 1353	1 wff -𝐴 = (0 − 𝐴)

This definition is referenced by:  negeq  8149  nfnegd  8152  csbnegg  8154  negcl  8156  neg0  8202  negid  8203  negsub  8204  subneg  8205  negneg  8206  negsubdi  8212  renegcl  8217  mulneg1  8351  ltneg  8418  leneg  8421  ixi  8539  0mnnnnn0  9207  fzshftral  10107  bernneq2  10641  cji  10910  bdtri  11247  prmdiv  12234  pcrec  12307  pcid  12322  4sqlem6  12380  4sqlem10  12384  sin0pilem1  14172  cospi  14191  coshalfpip  14213  ptolemy  14215  logbrec  14348  lgslem4  14374