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:be

Assertion

Ref	Expression
ax-wl	|- \x:al T:(al -> be)

Detailed syntax breakdown of Axiom ax-wl

Step	Hyp	Ref	Expression
1		hal	. . 3 type al
2		hbe	. . 3 type be
3	1, 2	ht 2	. 2 type (al -> be)
4		vx	. . 3 var x
5		tt	. . 3 term T
6	1, 4, 5	kl 6	. 2 term \x:al T
7	3, 6	wffMMJ2t 12	1 wff \x:al T:(al -> be)

This axiom is referenced by:  wl  66