Definition df-neg 8219

Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction (−) to prevent syntax ambiguity. See cneg 8217 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 8217	. 2 class -𝐴
3		cc0 7898	. . 3 class 0
4		cmin 8216	. . 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  8238  nfnegd  8241  csbnegg  8243  negcl  8245  neg0  8291  negid  8292  negsub  8293  subneg  8294  negneg  8295  negsubdi  8301  renegcl  8306  mulneg1  8440  ltneg  8508  leneg  8511  ixi  8629  0mnnnnn0  9300  fzshftral  10202  bernneq2  10772  cji  11086  bdtri  11424  m1bits  12144  bitsinv1lem  12145  prmdiv  12430  pcrec  12504  pcid  12520  4sqlem6  12579  4sqlem10  12583  sin0pilem1  15125  cospi  15144  coshalfpip  15166  ptolemy  15168  logbrec  15304  1sgm2ppw  15339  lgslem4  15352  lgseisen  15423