Definition df-neg 8463

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

This definition is referenced by:  negeq  8482  nfnegd  8485  csbnegg  8487  negcl  8489  neg0  8535  negid  8536  negsub  8537  subneg  8538  negneg  8539  negsubdi  8545  renegcl  8550  addeq0  8666  mulneg1  8685  ltneg  8753  leneg  8756  ixi  8874  0mnnnnn0  9545  fzshftral  10464  bernneq2  11048  cji  11612  bdtri  11950  m1bits  12671  bitsinv1lem  12672  prmdiv  12957  pcrec  13031  pcid  13047  4sqlem6  13106  4sqlem10  13110  ballotfilem1c  13195  sin0pilem1  15772  cospi  15791  coshalfpip  15813  ptolemy  15815  logbrec  15951  1sgm2ppw  15989  lgslem4  16002  lgseisen  16073  qdiff  16959