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

Definition df-al 126
Description: Define the for all operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
Assertion
Ref Expression
df-al ⊤⊧[ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]
Distinct variable group:   x,p

Detailed syntax breakdown of Definition df-al
StepHypRef Expression
1 kt 8 . 2 term
2 tal 122 . . 3 term
3 hal . . . . 5 type α
4 hb 3 . . . . 5 type
53, 4ht 2 . . . 4 type (α → ∗)
6 vp . . . 4 var p
75, 6tv 1 . . . . 5 term p:(α → ∗)
8 vx . . . . . 6 var x
93, 8, 1kl 6 . . . . 5 term λx:α
10 ke 7 . . . . 5 term =
117, 9, 10kbr 9 . . . 4 term [p:(α → ∗) = λx:α ⊤]
125, 6, 11kl 6 . . 3 term λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]
132, 12, 10kbr 9 . 2 term [ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]
141, 13wffMMJ2 11 1 wff ⊤⊧[ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]
Colors of variables: type var term
This definition is referenced by:  wal  134  alval  142
  Copyright terms: Public domain W3C validator