Definition df-neg 8316

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

This definition is referenced by:  negeq  8335  nfnegd  8338  csbnegg  8340  negcl  8342  neg0  8388  negid  8389  negsub  8390  subneg  8391  negneg  8392  negsubdi  8398  renegcl  8403  mulneg1  8537  ltneg  8605  leneg  8608  ixi  8726  0mnnnnn0  9397  fzshftral  10300  bernneq2  10878  cji  11408  bdtri  11746  m1bits  12466  bitsinv1lem  12467  prmdiv  12752  pcrec  12826  pcid  12842  4sqlem6  12901  4sqlem10  12905  sin0pilem1  15449  cospi  15468  coshalfpip  15490  ptolemy  15492  logbrec  15628  1sgm2ppw  15663  lgslem4  15676  lgseisen  15747