Definition wabs 162

Description: Type of the abstraction 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
wabs	⊢ A:(α → β)

Detailed syntax breakdown of Definition wabs

Step	Hyp	Ref	Expression
1		hal	. . 3 type α
2		hbe	. . 3 type β
3	1, 2	ht 2	. 2 type (α → β)
4		ta	. 2 term A
5	3, 4	wffMMJ2t 12	1 wff A:(α → β)

This definition is referenced by: (None)