Definition df-neg 8493

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

This definition is referenced by:  negeq  8512  nfnegd  8515  csbnegg  8517  negcl  8519  neg0  8565  negid  8566  negsub  8567  subneg  8568  negneg  8569  negsubdi  8575  renegcl  8580  addeq0  8696  mulneg1  8715  ltneg  8783  leneg  8786  ixi  8904  0mnnnnn0  9577  fzshftral  10496  bernneq2  11080  cji  11649  bdtri  11987  m1bits  12708  bitsinv1lem  12709  prmdiv  12994  pcrec  13068  pcid  13084  4sqlem6  13143  4sqlem10  13147  ballotfilem1c  13232  sin0pilem1  15808  cospi  15827  coshalfpip  15849  ptolemy  15851  logbrec  15988  1sgm2ppw  16026  lgslem4  16039  lgseisen  16110  qdiff  17006