Definition df-neg 7600

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 7598 for a discussion of this. (Contributed by NM, 10-Feb-1995.)

Assertion

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

Detailed syntax breakdown of Definition df-neg

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cneg 7598	. 2 class -u A
3		cc0 7294	. . 3 class 0
4		cmin 7597	. . 3 class -
5	3, 1, 4	co 5613	. 2 class ( 0 - A )
6	2, 5	wceq 1287	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  7619  nfnegd  7622  csbnegg  7624  negcl  7626  neg0  7672  negid  7673  negsub  7674  subneg  7675  negneg  7676  negsubdi  7682  renegcl  7687  mulneg1  7817  ltneg  7884  leneg  7887  ixi  8001  0mnnnnn0  8638  fzshftral  9452  bernneq2  9972  cji  10232