Definition df-neg 8131

Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction (−) to prevent syntax ambiguity. See cneg 8129 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 8129	. 2 class -𝐴
3		cc0 7811	. . 3 class 0
4		cmin 8128	. . 3 class −
5	3, 1, 4	co 5875	. 2 class (0 − 𝐴)
6	2, 5	wceq 1353	1 wff -𝐴 = (0 − 𝐴)

This definition is referenced by:  negeq  8150  nfnegd  8153  csbnegg  8155  negcl  8157  neg0  8203  negid  8204  negsub  8205  subneg  8206  negneg  8207  negsubdi  8213  renegcl  8218  mulneg1  8352  ltneg  8419  leneg  8422  ixi  8540  0mnnnnn0  9208  fzshftral  10108  bernneq2  10642  cji  10911  bdtri  11248  prmdiv  12235  pcrec  12308  pcid  12323  4sqlem6  12381  4sqlem10  12385  sin0pilem1  14205  cospi  14224  coshalfpip  14246  ptolemy  14248  logbrec  14381  lgslem4  14407