HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  wabs Unicode version
Definition wabs 162
Description: Type of the abstraction function.
Hypotheses
Ref Expression
ax-tdef.1 |- B:al
ax-tdef.2 |- F:(al -> *)
ax-tdef.3 |- T. |= (FB)
ax-tdef.4 |- typedef be(A, R)F
Assertion
Ref Expression
wabs |- A:(al -> be)
Detailed syntax breakdown of Definition wabs
StepHypRef Expression
1 hal . . 3 type al
2 hbe . . 3 type be
31, 2ht 2 . 2 type (al -> be)
4 ta . 2 term A
53, 4wffMMJ2t 12 1 wff A:(al -> be)
Colors of variables: type var term
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator