Axiom ax-wat 192

Description: The type of the indefinite descriptor. (New usage is discouraged.) (Contributed by Mario Carneiro, 10-Oct-2014.)

Assertion

Ref	Expression
ax-wat	⊢ ε:((α → ∗) → α)

Detailed syntax breakdown of Axiom ax-wat

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

This axiom is referenced by:  wat  193