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

Definition df-neg 7247
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 7245 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 7245 . 2  class  -u A
3 cc0 6946 . . 3  class  0
4 cmin 7244 . . 3  class  -
53, 1, 4co 5539 . 2  class  ( 0  -  A )
62, 5wceq 1259 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  7266  nfnegd  7269  csbnegg  7271  negcl  7273  neg0  7319  negid  7320  negsub  7321  subneg  7322  negneg  7323  negsubdi  7329  renegcl  7334  mulneg1  7463  ltneg  7530  leneg  7533  ixi  7647  0mnnnnn0  8270  fzshftral  9071  bernneq2  9537  cji  9729
  Copyright terms: Public domain W3C validator