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

Definition df-neg 7807
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 7805 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 7805 . 2  class  -u A
3 cc0 7500 . . 3  class  0
4 cmin 7804 . . 3  class  -
53, 1, 4co 5706 . 2  class  ( 0  -  A )
62, 5wceq 1299 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  7826  nfnegd  7829  csbnegg  7831  negcl  7833  neg0  7879  negid  7880  negsub  7881  subneg  7882  negneg  7883  negsubdi  7889  renegcl  7894  mulneg1  8024  ltneg  8091  leneg  8094  ixi  8211  0mnnnnn0  8861  fzshftral  9729  bernneq2  10254  cji  10515  bdtri  10850
  Copyright terms: Public domain W3C validator