Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > ax-hbl1 | Unicode version |
Description: is bound in . |
Ref | Expression |
---|---|
ax-hbl1.1 | |
ax-hbl1.2 |
Ref | Expression |
---|---|
ax-hbl1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | kt 8 | . 2 term | |
2 | hal | . . . . 5 type | |
3 | vx | . . . . 5 var | |
4 | hbe | . . . . . 6 type | |
5 | ta | . . . . . 6 term | |
6 | 4, 3, 5 | kl 6 | . . . . 5 term |
7 | 2, 3, 6 | kl 6 | . . . 4 term |
8 | tb | . . . 4 term | |
9 | 7, 8 | kc 5 | . . 3 term |
10 | ke 7 | . . 3 term | |
11 | 9, 6, 10 | kbr 9 | . 2 term |
12 | 1, 11 | wffMMJ2 11 | 1 wff |
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 |