Definition df-neg 8353

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

This definition is referenced by:  negeq  8372  nfnegd  8375  csbnegg  8377  negcl  8379  neg0  8425  negid  8426  negsub  8427  subneg  8428  negneg  8429  negsubdi  8435  renegcl  8440  mulneg1  8574  ltneg  8642  leneg  8645  ixi  8763  0mnnnnn0  9434  fzshftral  10343  bernneq2  10924  cji  11480  bdtri  11818  m1bits  12539  bitsinv1lem  12540  prmdiv  12825  pcrec  12899  pcid  12915  4sqlem6  12974  4sqlem10  12978  sin0pilem1  15524  cospi  15543  coshalfpip  15565  ptolemy  15567  logbrec  15703  1sgm2ppw  15738  lgslem4  15751  lgseisen  15822  qdiff  16704