Theorem wabs 174

Description: Type of the abstraction function. (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
wabs	|- A:(al -> be)

Proof of Theorem wabs

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

Syntax hints:   -> ht 2  *hb 3  kc 5  T.kt 8   |= wffMMJ2 11  wffMMJ2t 12  typedef wffMMJ2d 171

This theorem was proved from axioms:  ax-wabs 172

This theorem is referenced by: (None)