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

Theorem wabs 174
Description: Type of the abstraction function. (Contributed by Mario Carneiro, 8-Oct-2014.)
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
wabs A:(αβ)

Proof of Theorem wabs
StepHypRef Expression
1 ax-tdef.1 . 2 B:α
2 ax-tdef.2 . 2 F:(α → ∗)
3 ax-tdef.3 . 2 ⊤⊧(FB)
4 ax-tdef.4 . 2 typedef β(A, R)F
51, 2, 3, 4ax-wabs 172 1 A:(αβ)
Colors of variables: type var term
Syntax hints:  ht 2  hb 3  kc 5  kt 8  wffMMJ2 11  wffMMJ2t 12  typedef wffMMJ2d 171
This theorem was proved from axioms:  ax-wabs 172
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator