Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > ax-17 | Unicode version |
Description: If does not appear in , then any substitution to yields again, i.e. is a constant function. |
Ref | Expression |
---|---|
ax-17.1 | |
ax-17.2 |
Ref | Expression |
---|---|
ax-17 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | kt 8 | . 2 term | |
2 | hal | . . . . 5 type | |
3 | vx | . . . . 5 var | |
4 | ta | . . . . 5 term | |
5 | 2, 3, 4 | kl 6 | . . . 4 term |
6 | tb | . . . 4 term | |
7 | 5, 6 | kc 5 | . . 3 term |
8 | ke 7 | . . 3 term | |
9 | 7, 4, 8 | kbr 9 | . 2 term |
10 | 1, 9 | wffMMJ2 11 | 1 wff |
Colors of variables: type var term |
This axiom is referenced by: a17i 96 insti 104 cl 106 exlimdv 157 cbvf 167 cbv 168 leqf 169 exlimd 171 alimdv 172 eximdv 173 alnex 174 exmid 186 ax5 194 ax6 195 ax7 196 ax9 199 ax12 202 ax17 205 axext 206 axrep 207 |
Copyright terms: Public domain | W3C validator |