Definition df-neg 7960

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

This definition is referenced by:  negeq  7979  nfnegd  7982  csbnegg  7984  negcl  7986  neg0  8032  negid  8033  negsub  8034  subneg  8035  negneg  8036  negsubdi  8042  renegcl  8047  mulneg1  8181  ltneg  8248  leneg  8251  ixi  8369  0mnnnnn0  9033  fzshftral  9919  bernneq2  10444  cji  10706  bdtri  11043  sin0pilem1  12910  cospi  12929  coshalfpip  12951  ptolemy  12953  logbrec  13085