Definition df-neg 8245

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

This definition is referenced by:  negeq  8264  nfnegd  8267  csbnegg  8269  negcl  8271  neg0  8317  negid  8318  negsub  8319  subneg  8320  negneg  8321  negsubdi  8327  renegcl  8332  mulneg1  8466  ltneg  8534  leneg  8537  ixi  8655  0mnnnnn0  9326  fzshftral  10229  bernneq2  10804  cji  11184  bdtri  11522  m1bits  12242  bitsinv1lem  12243  prmdiv  12528  pcrec  12602  pcid  12618  4sqlem6  12677  4sqlem10  12681  sin0pilem1  15224  cospi  15243  coshalfpip  15265  ptolemy  15267  logbrec  15403  1sgm2ppw  15438  lgslem4  15451  lgseisen  15522