Definition df-neg 8281

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

This definition is referenced by:  negeq  8300  nfnegd  8303  csbnegg  8305  negcl  8307  neg0  8353  negid  8354  negsub  8355  subneg  8356  negneg  8357  negsubdi  8363  renegcl  8368  mulneg1  8502  ltneg  8570  leneg  8573  ixi  8691  0mnnnnn0  9362  fzshftral  10265  bernneq2  10843  cji  11328  bdtri  11666  m1bits  12386  bitsinv1lem  12387  prmdiv  12672  pcrec  12746  pcid  12762  4sqlem6  12821  4sqlem10  12825  sin0pilem1  15368  cospi  15387  coshalfpip  15409  ptolemy  15411  logbrec  15547  1sgm2ppw  15582  lgslem4  15595  lgseisen  15666