Definition df-neg 8063

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 8061 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 8061	. 2 class -u A
3		cc0 7744	. . 3 class 0
4		cmin 8060	. . 3 class -
5	3, 1, 4	co 5836	. 2 class ( 0 - A )
6	2, 5	wceq 1342	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  8082  nfnegd  8085  csbnegg  8087  negcl  8089  neg0  8135  negid  8136  negsub  8137  subneg  8138  negneg  8139  negsubdi  8145  renegcl  8150  mulneg1  8284  ltneg  8351  leneg  8354  ixi  8472  0mnnnnn0  9137  fzshftral  10033  bernneq2  10565  cji  10830  bdtri  11167  prmdiv  12144  pcrec  12217  pcid  12232  sin0pilem1  13243  cospi  13262  coshalfpip  13284  ptolemy  13286  logbrec  13419