Definition df-neg 8068

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

This definition is referenced by:  negeq  8087  nfnegd  8090  csbnegg  8092  negcl  8094  neg0  8140  negid  8141  negsub  8142  subneg  8143  negneg  8144  negsubdi  8150  renegcl  8155  mulneg1  8289  ltneg  8356  leneg  8359  ixi  8477  0mnnnnn0  9142  fzshftral  10039  bernneq2  10572  cji  10840  bdtri  11177  prmdiv  12163  pcrec  12236  pcid  12251  4sqlem6  12309  4sqlem10  12313  sin0pilem1  13302  cospi  13321  coshalfpip  13343  ptolemy  13345  logbrec  13478  lgslem4  13504