Definition df-neg 7282

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 7280 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 7280	. 2 class -u A
3		cc0 6981	. . 3 class 0
4		cmin 7279	. . 3 class -
5	3, 1, 4	co 5532	. 2 class ( 0 - A )
6	2, 5	wceq 1284	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  7301  nfnegd  7304  csbnegg  7306  negcl  7308  neg0  7354  negid  7355  negsub  7356  subneg  7357  negneg  7358  negsubdi  7364  renegcl  7369  mulneg1  7499  ltneg  7566  leneg  7569  ixi  7683  0mnnnnn0  8320  fzshftral  9125  bernneq2  9594  cji  9789