Definition df-neg 10588

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

This definition is referenced by:  negeq  10593  nfnegd  10596  csbnegg  10598  negex  10599  negcl  10601  neg0  10648  negid  10649  negsub  10650  subneg  10651  negneg  10652  negsubdi  10658  renegcli  10663  addeq0  10777  mulneg1  10790  ltneg  10852  leneg  10855  ixi  10981  0mnnnnn0  11652  max0sub  12315  fzshftral  12722  bernneq2  13285  discr1  13294  discr  13295  cji  14276  rlimrege0  14687  rlimneg  14754  risefall0lem  15129  fallfacfwd  15139  binomfallfaclem2  15143  fsumcube  15163  divalglem1  15491  divalglem2  15492  m1bits  15535  bitsinv1lem  15536  prmdiv  15861  pcrec  15934  pcid  15948  4sqlem6  16018  4sqlem10  16022  psgnunilem2  18266  cnheibor  23124  evth2  23129  dvlipcn  24156  dvfsumge  24184  ftc2  24206  vieta1lem2  24465  abelthlem8  24592  cospi  24624  coshalfpip  24646  ptolemy  24648  pige3  24669  tanregt0  24685  argimgt0  24757  logcnlem3  24789  logf1o2  24795  advlogexp  24800  logtayl  24805  dvsqrt  24885  dvcnsqrt  24887  cxpcn3  24891  ang180lem3  24951  isosctrlem2  24959  asinlem  25008  atancj  25050  atanlogaddlem  25053  atantan  25063  dvatan  25075  emcllem7  25141  dmgmaddn0  25162  lgamgulmlem5  25172  lgambdd  25176  ftalem3  25214  1sgm2ppw  25338  dchrfi  25393  lgslem4  25438  lgseisen  25517  log2sumbnd  25646  colinearalglem4  26208  qqhcn  30580  ballotlem1c  31115  sgnneg  31148  quad3  32108  fz0n  32158  climlec3  32161  fwddifnp1  32811  tan2h  33944  broucube  33987  ftc2nc  34037  dvasin  34039  dvacos  34040  areacirclem1  34043  mzpnegmpt  38151  binomcxplemrat  39389  binomcxplemnotnn0  39395  negcncfg  40889  itgsinexplem1  40964  stoweidlem34  41045  stirlinglem5  41089  fourierdlem36  41154  fourierdlem89  41206  fourierdlem90  41207  fourierdlem91  41208  fourierdlem107  41224  etransclem9  41254  etransclem14  41259  etransclem28  41273  etransclem35  41280  etransclem46  41291  0nodd  42657  m1modmmod  43163  line2  43304