Definition df-neg 7936

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

This definition is referenced by:  negeq  7955  nfnegd  7958  csbnegg  7960  negcl  7962  neg0  8008  negid  8009  negsub  8010  subneg  8011  negneg  8012  negsubdi  8018  renegcl  8023  mulneg1  8157  ltneg  8224  leneg  8227  ixi  8345  0mnnnnn0  9009  fzshftral  9888  bernneq2  10413  cji  10674  bdtri  11011  sin0pilem1  12862  cospi  12881  coshalfpip  12903  ptolemy  12905