Definition df-neg 11495

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

This definition is referenced by:  negeq  11500  nfnegd  11503  csbnegg  11505  negex  11506  negcl  11508  neg0  11555  negid  11556  negsub  11557  subneg  11558  negneg  11559  negsubdi  11565  renegcli  11570  addeq0  11686  mulneg1  11699  mulsubaddmulsub  11727  ltneg  11763  leneg  11766  ixi  11892  0mnnnnn0  12558  max0sub  13238  fzshftral  13655  bernneq2  14269  discr1  14278  discr  14279  cji  15198  rlimrege0  15615  rlimneg  15683  risefall0lem  16062  fallfacfwd  16072  binomfallfaclem2  16076  fsumcube  16096  divalglem1  16431  divalglem2  16432  m1bits  16477  bitsinv1lem  16478  prmdiv  16822  pcrec  16896  pcid  16911  4sqlem6  16981  4sqlem10  16985  psgnunilem2  19513  cnheibor  24987  evth2  24992  dvlipcn  26033  dvfsumge  26062  ftc2  26085  vieta1lem2  26353  abelthlem8  26483  cospi  26514  coshalfpip  26536  ptolemy  26538  pige3ALT  26562  tanregt0  26581  argimgt0  26654  logcnlem3  26686  logf1o2  26692  advlogexp  26697  logtayl  26702  dvsqrt  26784  dvcnsqrt  26786  cxpcn3  26791  ang180lem3  26854  isosctrlem2  26862  asinlem  26911  atancj  26953  atanlogaddlem  26956  atantan  26966  dvatan  26978  emcllem7  27045  dmgmaddn0  27066  lgamgulmlem5  27076  lgambdd  27080  ftalem3  27118  1sgm2ppw  27244  dchrfi  27299  lgslem4  27344  lgseisen  27423  log2sumbnd  27588  colinearalglem4  28924  re0cj  32753  quad3d  32754  chnub  33002  constrrtcc  33776  constrelextdg2  33788  2sqr3minply  33791  qqhcn  33992  ballotlem1c  34510  sgnneg  34543  quad3  35675  fz0n  35731  climlec3  35734  fwddifnp1  36166  tan2h  37619  broucube  37661  ftc2nc  37709  dvasin  37711  dvacos  37712  areacirclem1  37715  lcmineqlem7  42036  lcmineqlem10  42039  lcmineqlem12  42041  aks4d1p1p7  42075  posbezout  42101  bcle2d  42180  aks6d1c7lem1  42181  reelznn0nn  42479  mzpnegmpt  42755  binomcxplemrat  44369  binomcxplemnotnn0  44375  negcncfg  45896  itgsinexplem1  45969  stoweidlem34  46049  stirlinglem5  46093  fourierdlem36  46158  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem107  46228  etransclem9  46258  etransclem14  46263  etransclem28  46277  etransclem35  46284  etransclem46  46295  resubcnnred  47316  gpgedgvtx0  48019  gpg3kgrtriex  48045  0nodd  48086  m1modmmod  48442  line2  48673  itschlc0xyqsol  48688