Nearby theorems
|
|
Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > HOLE Home > Th. List > wrep | GIF version | ||
| Description: Type of the representation function. |
| Ref | Expression |
|---|---|
| ax-tdef.1 | ⊢ B:α |
| ax-tdef.2 | ⊢ F:(α → ∗) |
| ax-tdef.3 | ⊢ ⊤⊧(FB) |
| ax-tdef.4 | ⊢ typedef β(A, R)F |
| Ref | Expression |
|---|---|
| wrep | ⊢ R:(β → α) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hbe | . . 3 type β | |
| 2 | hal | . . 3 type α | |
| 3 | 1, 2 | ht 2 | . 2 type (β → α) |
| 4 | tr | . 2 term R | |
| 5 | 3, 4 | wffMMJ2t 12 | 1 wff R:(β → α) |
| Colors of variables: type var term |
| This definition is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |