Definition df-neg 8449

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

This definition is referenced by:  negeq  8468  nfnegd  8471  csbnegg  8473  negcl  8475  neg0  8521  negid  8522  negsub  8523  subneg  8524  negneg  8525  negsubdi  8531  renegcl  8536  mulneg1  8670  ltneg  8738  leneg  8741  ixi  8859  0mnnnnn0  9530  fzshftral  10446  bernneq2  11027  cji  11591  bdtri  11929  m1bits  12650  bitsinv1lem  12651  prmdiv  12936  pcrec  13010  pcid  13026  4sqlem6  13085  4sqlem10  13089  sin0pilem1  15663  cospi  15682  coshalfpip  15704  ptolemy  15706  logbrec  15842  1sgm2ppw  15880  lgslem4  15893  lgseisen  15964  qdiff  16850