Definition df-neg 7717

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

This definition is referenced by:  negeq  7736  nfnegd  7739  csbnegg  7741  negcl  7743  neg0  7789  negid  7790  negsub  7791  subneg  7792  negneg  7793  negsubdi  7799  renegcl  7804  mulneg1  7934  ltneg  8001  leneg  8004  ixi  8121  0mnnnnn0  8766  fzshftral  9583  bernneq2  10136  cji  10397