Definition df-neg 8502

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

This definition is used by:  negeq  8521  nfnegd  8524  csbnegg  8526  negcl  8528  neg0  8574  negid  8575  negsub  8576  subneg  8577  negneg  8578  negsubdi  8584  renegcl  8589  addeq0  8705  mulneg1  8724  ltneg  8792  leneg  8795  ixi  8914  0mnnnnn0  9600  fz00m1  10462  fzshftral  10526  bernneq2  11114  cji  11684  bdtri  12025  m1bits  12746  bitsinv1lem  12747  prmdiv  13036  pcrec  13110  pcid  13126  4sqlem6  13185  4sqlem10  13189  ballotfilem1c  13303  sin0pilem1  15974  cospi  15993  coshalfpip  16015  ptolemy  16017  logbrec  16157  1sgm2ppw  16250  lgslem4  16288  lgseisen  16359  qdiff  17265