HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  wrep GIF version

Definition wrep 163
Description: Type of the representation function.
Hypotheses
Ref Expression
ax-tdef.1 B:α
ax-tdef.2 F:(α → ∗)
ax-tdef.3 ⊤⊧(FB)
ax-tdef.4 typedef β(A, R)F
Assertion
Ref Expression
wrep R:(βα)

Detailed syntax breakdown of Definition wrep
StepHypRef Expression
1 hbe . . 3 type β
2 hal . . 3 type α
31, 2ht 2 . 2 type (βα)
4 tr . 2 term R
53, 4wffMMJ2t 12 1 wff R:(βα)
Colors of variables: type var term
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator