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

Definition df-neg 7426
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 7424 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 7424 . 2  class  -u A
3 cc0 7120 . . 3  class  0
4 cmin 7423 . . 3  class  -
53, 1, 4co 5565 . 2  class  ( 0  -  A )
62, 5wceq 1285 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  7445  nfnegd  7448  csbnegg  7450  negcl  7452  neg0  7498  negid  7499  negsub  7500  subneg  7501  negneg  7502  negsubdi  7508  renegcl  7513  mulneg1  7643  ltneg  7710  leneg  7713  ixi  7827  0mnnnnn0  8464  fzshftral  9278  bernneq2  9768  cji  10015
  Copyright terms: Public domain W3C validator