Definition df-neg 8331

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

This definition is referenced by:  negeq  8350  nfnegd  8353  csbnegg  8355  negcl  8357  neg0  8403  negid  8404  negsub  8405  subneg  8406  negneg  8407  negsubdi  8413  renegcl  8418  mulneg1  8552  ltneg  8620  leneg  8623  ixi  8741  0mnnnnn0  9412  fzshftral  10316  bernneq2  10895  cji  11428  bdtri  11766  m1bits  12486  bitsinv1lem  12487  prmdiv  12772  pcrec  12846  pcid  12862  4sqlem6  12921  4sqlem10  12925  sin0pilem1  15470  cospi  15489  coshalfpip  15511  ptolemy  15513  logbrec  15649  1sgm2ppw  15684  lgslem4  15697  lgseisen  15768