Definition df-neg 8217

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

This definition is referenced by:  negeq  8236  nfnegd  8239  csbnegg  8241  negcl  8243  neg0  8289  negid  8290  negsub  8291  subneg  8292  negneg  8293  negsubdi  8299  renegcl  8304  mulneg1  8438  ltneg  8506  leneg  8509  ixi  8627  0mnnnnn0  9298  fzshftral  10200  bernneq2  10770  cji  11084  bdtri  11422  m1bits  12142  bitsinv1lem  12143  prmdiv  12428  pcrec  12502  pcid  12518  4sqlem6  12577  4sqlem10  12581  sin0pilem1  15101  cospi  15120  coshalfpip  15142  ptolemy  15144  logbrec  15280  1sgm2ppw  15315  lgslem4  15328  lgseisen  15399