ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-neg Unicode version

Definition df-neg 7956
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 7954 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
StepHypRef Expression
1 cA . . 3  class  A
21cneg 7954 . 2  class  -u A
3 cc0 7640 . . 3  class  0
4 cmin 7953 . . 3  class  -
53, 1, 4co 5778 . 2  class  ( 0  -  A )
62, 5wceq 1332 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  7975  nfnegd  7978  csbnegg  7980  negcl  7982  neg0  8028  negid  8029  negsub  8030  subneg  8031  negneg  8032  negsubdi  8038  renegcl  8043  mulneg1  8177  ltneg  8244  leneg  8247  ixi  8365  0mnnnnn0  9029  fzshftral  9915  bernneq2  10440  cji  10702  bdtri  11039  sin0pilem1  12901  cospi  12920  coshalfpip  12942  ptolemy  12944  logbrec  13076
  Copyright terms: Public domain W3C validator