HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  df-not GIF version

Definition df-not 120
Description: Define the negation operator.
Assertion
Ref Expression
df-not ⊤⊧[¬ = λp:∗ [p:∗ ⇒ ⊥]]

Detailed syntax breakdown of Definition df-not
StepHypRef Expression
1 kt 8 . 2 term
2 tne 110 . . 3 term ¬
3 hb 3 . . . 4 type
4 vp . . . 4 var p
53, 4tv 1 . . . . 5 term p:∗
6 tfal 108 . . . . 5 term
7 tim 111 . . . . 5 term
85, 6, 7kbr 9 . . . 4 term [p:∗ ⇒ ⊥]
93, 4, 8kl 6 . . 3 term λp:∗ [p:∗ ⇒ ⊥]
10 ke 7 . . 3 term =
112, 9, 10kbr 9 . 2 term [¬ = λp:∗ [p:∗ ⇒ ⊥]]
121, 11wffMMJ2 11 1 wff ⊤⊧[¬ = λp:∗ [p:∗ ⇒ ⊥]]
Colors of variables: type var term
This definition is referenced by:  wnot  128  notval  135
  Copyright terms: Public domain W3C validator