Definition df-neg 8246

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

This definition is referenced by:  negeq  8265  nfnegd  8268  csbnegg  8270  negcl  8272  neg0  8318  negid  8319  negsub  8320  subneg  8321  negneg  8322  negsubdi  8328  renegcl  8333  mulneg1  8467  ltneg  8535  leneg  8538  ixi  8656  0mnnnnn0  9327  fzshftral  10230  bernneq2  10806  cji  11213  bdtri  11551  m1bits  12271  bitsinv1lem  12272  prmdiv  12557  pcrec  12631  pcid  12647  4sqlem6  12706  4sqlem10  12710  sin0pilem1  15253  cospi  15272  coshalfpip  15294  ptolemy  15296  logbrec  15432  1sgm2ppw  15467  lgslem4  15480  lgseisen  15551