Axiom ax-weq 40

Description: The equality function has type α → α → ∗, i.e. it is polymorphic over all types, but the left and right type must agree. (New usage is discouraged.) (Contributed by Mario Carneiro, 7-Oct-2014.)

Assertion

Ref	Expression
ax-weq	⊢ = :(α → (α → ∗))

Detailed syntax breakdown of Axiom ax-weq

Step	Hyp	Ref	Expression
1		hal	. . 3 type α
2		hb 3	. . . 4 type ∗
3	1, 2	ht 2	. . 3 type (α → ∗)
4	1, 3	ht 2	. 2 type (α → (α → ∗))
5		ke 7	. 2 term =
6	4, 5	wffMMJ2t 12	1 wff = :(α → (α → ∗))

This axiom is referenced by:  weq  41