Definition df-neg 11208

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

This definition is referenced by:  negeq  11213  nfnegd  11216  csbnegg  11218  negex  11219  negcl  11221  neg0  11267  negid  11268  negsub  11269  subneg  11270  negneg  11271  negsubdi  11277  renegcli  11282  addeq0  11398  mulneg1  11411  mulsubaddmulsub  11439  ltneg  11475  leneg  11478  ixi  11604  0mnnnnn0  12265  max0sub  12930  fzshftral  13344  bernneq2  13945  discr1  13954  discr  13955  cji  14870  rlimrege0  15288  rlimneg  15358  risefall0lem  15736  fallfacfwd  15746  binomfallfaclem2  15750  fsumcube  15770  divalglem1  16103  divalglem2  16104  m1bits  16147  bitsinv1lem  16148  prmdiv  16486  pcrec  16559  pcid  16574  4sqlem6  16644  4sqlem10  16648  psgnunilem2  19103  cnheibor  24118  evth2  24123  dvlipcn  25158  dvfsumge  25186  ftc2  25208  vieta1lem2  25471  abelthlem8  25598  cospi  25629  coshalfpip  25651  ptolemy  25653  pige3ALT  25676  tanregt0  25695  argimgt0  25767  logcnlem3  25799  logf1o2  25805  advlogexp  25810  logtayl  25815  dvsqrt  25895  dvcnsqrt  25897  cxpcn3  25901  ang180lem3  25961  isosctrlem2  25969  asinlem  26018  atancj  26060  atanlogaddlem  26063  atantan  26073  dvatan  26085  emcllem7  26151  dmgmaddn0  26172  lgamgulmlem5  26182  lgambdd  26186  ftalem3  26224  1sgm2ppw  26348  dchrfi  26403  lgslem4  26448  lgseisen  26527  log2sumbnd  26692  colinearalglem4  27277  qqhcn  31941  ballotlem1c  32474  sgnneg  32507  quad3  33628  fz0n  33696  climlec3  33699  fwddifnp1  34467  tan2h  35769  broucube  35811  ftc2nc  35859  dvasin  35861  dvacos  35862  areacirclem1  35865  lcmineqlem7  40043  lcmineqlem10  40046  lcmineqlem12  40048  aks4d1p1p7  40082  mzpnegmpt  40566  binomcxplemrat  41968  binomcxplemnotnn0  41974  negcncfg  43422  itgsinexplem1  43495  stoweidlem34  43575  stirlinglem5  43619  fourierdlem36  43684  fourierdlem89  43736  fourierdlem90  43737  fourierdlem91  43738  fourierdlem107  43754  etransclem9  43784  etransclem14  43789  etransclem28  43803  etransclem35  43810  etransclem46  43821  resubcnnred  44796  0nodd  45364  m1modmmod  45867  line2  46098  itschlc0xyqsol  46113