Axiom ax-wabs 172

Description: Type of the abstraction function. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
ax-tdef.1	|- B:al
ax-tdef.2	|- F:(al -> *)
ax-tdef.3	|- T. |= (FB)
ax-tdef.4	|- typedef be(A, R)F

Assertion

Ref	Expression
ax-wabs	|- A:(al -> be)

Detailed syntax breakdown of Axiom ax-wabs

Step	Hyp	Ref	Expression
1		hal	. . 3 type al
2		hbe	. . 3 type be
3	1, 2	ht 2	. 2 type (al -> be)
4		ta	. 2 term A
5	3, 4	wffMMJ2t 12	1 wff A:(al -> be)

This axiom is referenced by:  wabs  174