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

Definition df-fal 127
Description: Define the constant false. (Contributed by Mario Carneiro, 8-Oct-2014.)
Assertion
Ref Expression
df-fal ⊤⊧[⊥ = (λp:∗ p:∗)]

Detailed syntax breakdown of Definition df-fal
StepHypRef Expression
1 kt 8 . 2 term
2 tfal 118 . . 3 term
3 tal 122 . . . 4 term
4 hb 3 . . . . 5 type
5 vp . . . . 5 var p
64, 5tv 1 . . . . 5 term p:∗
74, 5, 6kl 6 . . . 4 term λp:∗ p:∗
83, 7kc 5 . . 3 term (λp:∗ p:∗)
9 ke 7 . . 3 term =
102, 8, 9kbr 9 . 2 term [⊥ = (λp:∗ p:∗)]
111, 10wffMMJ2 11 1 wff ⊤⊧[⊥ = (λp:∗ p:∗)]
Colors of variables: type var term
This definition is referenced by:  wfal  135  pm2.21  153
  Copyright terms: Public domain W3C validator