Definition df-neg 10873

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

This definition is referenced by:  negeq  10878  nfnegd  10881  csbnegg  10883  negex  10884  negcl  10886  neg0  10932  negid  10933  negsub  10934  subneg  10935  negneg  10936  negsubdi  10942  renegcli  10947  addeq0  11063  mulneg1  11076  mulsubaddmulsub  11104  ltneg  11140  leneg  11143  ixi  11269  0mnnnnn0  11930  max0sub  12590  fzshftral  12996  bernneq2  13592  discr1  13601  discr  13602  cji  14518  rlimrege0  14936  rlimneg  15003  risefall0lem  15380  fallfacfwd  15390  binomfallfaclem2  15394  fsumcube  15414  divalglem1  15745  divalglem2  15746  m1bits  15789  bitsinv1lem  15790  prmdiv  16122  pcrec  16195  pcid  16209  4sqlem6  16279  4sqlem10  16283  psgnunilem2  18623  cnheibor  23559  evth2  23564  dvlipcn  24591  dvfsumge  24619  ftc2  24641  vieta1lem2  24900  abelthlem8  25027  cospi  25058  coshalfpip  25080  ptolemy  25082  pige3ALT  25105  tanregt0  25123  argimgt0  25195  logcnlem3  25227  logf1o2  25233  advlogexp  25238  logtayl  25243  dvsqrt  25323  dvcnsqrt  25325  cxpcn3  25329  ang180lem3  25389  isosctrlem2  25397  asinlem  25446  atancj  25488  atanlogaddlem  25491  atantan  25501  dvatan  25513  emcllem7  25579  dmgmaddn0  25600  lgamgulmlem5  25610  lgambdd  25614  ftalem3  25652  1sgm2ppw  25776  dchrfi  25831  lgslem4  25876  lgseisen  25955  log2sumbnd  26120  colinearalglem4  26695  qqhcn  31232  ballotlem1c  31765  sgnneg  31798  quad3  32913  fz0n  32962  climlec3  32965  fwddifnp1  33626  tan2h  34899  broucube  34941  ftc2nc  34991  dvasin  34993  dvacos  34994  areacirclem1  34997  mzpnegmpt  39361  binomcxplemrat  40702  binomcxplemnotnn0  40708  negcncfg  42184  itgsinexplem1  42259  stoweidlem34  42339  stirlinglem5  42383  fourierdlem36  42448  fourierdlem89  42500  fourierdlem90  42501  fourierdlem91  42502  fourierdlem107  42518  etransclem9  42548  etransclem14  42553  etransclem28  42567  etransclem35  42574  etransclem46  42585  resubcnnred  43524  0nodd  44097  m1modmmod  44601  line2  44759  itschlc0xyqsol  44774