Definition df-neg 8343

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

This definition is referenced by:  negeq  8362  nfnegd  8365  csbnegg  8367  negcl  8369  neg0  8415  negid  8416  negsub  8417  subneg  8418  negneg  8419  negsubdi  8425  renegcl  8430  mulneg1  8564  ltneg  8632  leneg  8635  ixi  8753  0mnnnnn0  9424  fzshftral  10333  bernneq2  10913  cji  11453  bdtri  11791  m1bits  12511  bitsinv1lem  12512  prmdiv  12797  pcrec  12871  pcid  12887  4sqlem6  12946  4sqlem10  12950  sin0pilem1  15495  cospi  15514  coshalfpip  15536  ptolemy  15538  logbrec  15674  1sgm2ppw  15709  lgslem4  15722  lgseisen  15793