Definition df-neg 8412

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

This definition is referenced by:  negeq  8431  nfnegd  8434  csbnegg  8436  negcl  8438  neg0  8484  negid  8485  negsub  8486  subneg  8487  negneg  8488  negsubdi  8494  renegcl  8499  mulneg1  8633  ltneg  8701  leneg  8704  ixi  8822  0mnnnnn0  9493  fzshftral  10405  bernneq2  10986  cji  11542  bdtri  11880  m1bits  12601  bitsinv1lem  12602  prmdiv  12887  pcrec  12961  pcid  12977  4sqlem6  13036  4sqlem10  13040  sin0pilem1  15592  cospi  15611  coshalfpip  15633  ptolemy  15635  logbrec  15771  1sgm2ppw  15809  lgslem4  15822  lgseisen  15893  qdiff  16781