Definition df-neg 4135

Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-u) and subtraction (-) to prevent syntax ambiguity. See cneg 4090 for a discussion of this.

Assertion

Ref	Expression
df-neg	|- -uA = (0 - A)

Detailed syntax breakdown of Definition df-neg

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cneg 4090	. 2 class -uA
3		cc0 4028	. . 3 class 0
4		cmin 4089	. . 3 class -
5	3, 1, 4	co 3001	. 2 class (0 - A)
6	2, 5	wceq 1091	1 wff -uA = (0 - A)

This definition is referenced by:  negeq 4136  negclt 4141  negid 4147  neg11 4164  neg0 4170  renegcl 4171  mulneg1 4190  eqneg 4378  nn0subt 4587  discrlem3 4715  sqrlem11 4741

metamath.org