Axiom ax-wl 65

Description: The type of a lambda abstraction. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypothesis

Ref	Expression
wl.1	⊢ T:β

Assertion

Ref	Expression
ax-wl	⊢ λx:α T:(α → β)

Detailed syntax breakdown of Axiom ax-wl

Step	Hyp	Ref	Expression
1		hal	. . 3 type α
2		hbe	. . 3 type β
3	1, 2	ht 2	. 2 type (α → β)
4		vx	. . 3 var x
5		tt	. . 3 term T
6	1, 4, 5	kl 6	. 2 term λx:α T
7	3, 6	wffMMJ2t 12	1 wff λx:α T:(α → β)

This axiom is referenced by:  wl  66