Definition df-neg 10862

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

This definition is referenced by:  negeq  10867  nfnegd  10870  csbnegg  10872  negex  10873  negcl  10875  neg0  10921  negid  10922  negsub  10923  subneg  10924  negneg  10925  negsubdi  10931  renegcli  10936  addeq0  11052  mulneg1  11065  mulsubaddmulsub  11093  ltneg  11129  leneg  11132  ixi  11258  0mnnnnn0  11917  max0sub  12577  fzshftral  12990  bernneq2  13587  discr1  13596  discr  13597  cji  14510  rlimrege0  14928  rlimneg  14995  risefall0lem  15372  fallfacfwd  15382  binomfallfaclem2  15386  fsumcube  15406  divalglem1  15735  divalglem2  15736  m1bits  15779  bitsinv1lem  15780  prmdiv  16112  pcrec  16185  pcid  16199  4sqlem6  16269  4sqlem10  16273  psgnunilem2  18615  cnheibor  23560  evth2  23565  dvlipcn  24597  dvfsumge  24625  ftc2  24647  vieta1lem2  24907  abelthlem8  25034  cospi  25065  coshalfpip  25087  ptolemy  25089  pige3ALT  25112  tanregt0  25131  argimgt0  25203  logcnlem3  25235  logf1o2  25241  advlogexp  25246  logtayl  25251  dvsqrt  25331  dvcnsqrt  25333  cxpcn3  25337  ang180lem3  25397  isosctrlem2  25405  asinlem  25454  atancj  25496  atanlogaddlem  25499  atantan  25509  dvatan  25521  emcllem7  25587  dmgmaddn0  25608  lgamgulmlem5  25618  lgambdd  25622  ftalem3  25660  1sgm2ppw  25784  dchrfi  25839  lgslem4  25884  lgseisen  25963  log2sumbnd  26128  colinearalglem4  26703  qqhcn  31342  ballotlem1c  31875  sgnneg  31908  quad3  33026  fz0n  33075  climlec3  33078  fwddifnp1  33739  tan2h  35049  broucube  35091  ftc2nc  35139  dvasin  35141  dvacos  35142  areacirclem1  35145  lcmineqlem7  39323  lcmineqlem10  39326  lcmineqlem12  39328  mzpnegmpt  39685  binomcxplemrat  41054  binomcxplemnotnn0  41060  negcncfg  42523  itgsinexplem1  42596  stoweidlem34  42676  stirlinglem5  42720  fourierdlem36  42785  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem107  42855  etransclem9  42885  etransclem14  42890  etransclem28  42904  etransclem35  42911  etransclem46  42922  resubcnnred  43861  0nodd  44430  m1modmmod  44935  line2  45166  itschlc0xyqsol  45181