Definition df-neg 10896

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

This definition is referenced by:  negeq  10901  nfnegd  10904  csbnegg  10906  negex  10907  negcl  10909  neg0  10955  negid  10956  negsub  10957  subneg  10958  negneg  10959  negsubdi  10965  renegcli  10970  addeq0  11086  mulneg1  11099  mulsubaddmulsub  11127  ltneg  11163  leneg  11166  ixi  11292  0mnnnnn0  11951  max0sub  12615  fzshftral  13029  bernneq2  13626  discr1  13635  discr  13636  cji  14551  rlimrege0  14969  rlimneg  15036  risefall0lem  15413  fallfacfwd  15423  binomfallfaclem2  15427  fsumcube  15447  divalglem1  15780  divalglem2  15781  m1bits  15824  bitsinv1lem  15825  prmdiv  16162  pcrec  16235  pcid  16249  4sqlem6  16319  4sqlem10  16323  psgnunilem2  18675  cnheibor  23641  evth2  23646  dvlipcn  24678  dvfsumge  24706  ftc2  24728  vieta1lem2  24991  abelthlem8  25118  cospi  25149  coshalfpip  25171  ptolemy  25173  pige3ALT  25196  tanregt0  25215  argimgt0  25287  logcnlem3  25319  logf1o2  25325  advlogexp  25330  logtayl  25335  dvsqrt  25415  dvcnsqrt  25417  cxpcn3  25421  ang180lem3  25481  isosctrlem2  25489  asinlem  25538  atancj  25580  atanlogaddlem  25583  atantan  25593  dvatan  25605  emcllem7  25671  dmgmaddn0  25692  lgamgulmlem5  25702  lgambdd  25706  ftalem3  25744  1sgm2ppw  25868  dchrfi  25923  lgslem4  25968  lgseisen  26047  log2sumbnd  26212  colinearalglem4  26787  qqhcn  31445  ballotlem1c  31978  sgnneg  32011  quad3  33129  fz0n  33196  climlec3  33199  fwddifnp1  34001  tan2h  35314  broucube  35356  ftc2nc  35404  dvasin  35406  dvacos  35407  areacirclem1  35410  lcmineqlem7  39587  lcmineqlem10  39590  lcmineqlem12  39592  aks4d1p1p7  39625  mzpnegmpt  40043  binomcxplemrat  41412  binomcxplemnotnn0  41418  negcncfg  42874  itgsinexplem1  42947  stoweidlem34  43027  stirlinglem5  43071  fourierdlem36  43136  fourierdlem89  43188  fourierdlem90  43189  fourierdlem91  43190  fourierdlem107  43206  etransclem9  43236  etransclem14  43241  etransclem28  43255  etransclem35  43262  etransclem46  43273  resubcnnred  44214  0nodd  44782  m1modmmod  45285  line2  45516  itschlc0xyqsol  45531