Axiom ax-wv 63

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

Assertion

Ref	Expression
ax-wv	⊢ x:α:α

Detailed syntax breakdown of Axiom ax-wv

Step	Hyp	Ref	Expression
1		hal	. 2 type α
2		vx	. . 3 var x
3	1, 2	tv 1	. 2 term x:α
4	1, 3	wffMMJ2t 12	1 wff x:α:α

This axiom is referenced by:  wv  64