Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > ax-hbl1 | GIF version |
Description: x is bound in λxA. |
Ref | Expression |
---|---|
ax-hbl1.1 | ⊢ A:γ |
ax-hbl1.2 | ⊢ B:α |
Ref | Expression |
---|---|
ax-hbl1 | ⊢ ⊤⊧[(λx:α λx:β AB) = λx:β A] |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | kt 8 | . 2 term ⊤ | |
2 | hal | . . . . 5 type α | |
3 | vx | . . . . 5 var x | |
4 | hbe | . . . . . 6 type β | |
5 | ta | . . . . . 6 term A | |
6 | 4, 3, 5 | kl 6 | . . . . 5 term λx:β A |
7 | 2, 3, 6 | kl 6 | . . . 4 term λx:α λx:β A |
8 | tb | . . . 4 term B | |
9 | 7, 8 | kc 5 | . . 3 term (λx:α λx:β AB) |
10 | ke 7 | . . 3 term = | |
11 | 9, 6, 10 | kbr 9 | . 2 term [(λx:α λx:β AB) = λx:β A] |
12 | 1, 11 | wffMMJ2 11 | 1 wff ⊤⊧[(λx:α λx:β AB) = λx:β A] |
Colors of variables: type var term |
This axiom is referenced by: hbl1 94 exlimdv 157 leqf 169 exlimd 171 alimdv 172 eximdv 173 alnex 174 exmid 186 ax5 194 ax6 195 ax7 196 ax9 199 axext 206 axrep 207 |
Copyright terms: Public domain | W3C validator |