Theorem wabs 174

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

Hypotheses

Ref	Expression
ax-tdef.1	⊢ B:α
ax-tdef.2	⊢ F:(α → ∗)
ax-tdef.3	⊢ ⊤⊧(FB)
ax-tdef.4	⊢ typedef β(A, R)F

Assertion

Ref	Expression
wabs	⊢ A:(α → β)

Proof of Theorem wabs

Step	Hyp	Ref	Expression
1		ax-tdef.1	. 2 ⊢ B:α
2		ax-tdef.2	. 2 ⊢ F:(α → ∗)
3		ax-tdef.3	. 2 ⊢ ⊤⊧(FB)
4		ax-tdef.4	. 2 ⊢ typedef β(A, R)F
5	1, 2, 3, 4	ax-wabs 172	1 ⊢ A:(α → β)

This proof depends on syntax axioms:   → ht 2  ∗hb 3  kc 5  ⊤kt 8  ⊧wffMMJ2 11  wffMMJ2t 12  typedef wffMMJ2d 171

This proof depends on axioms:  ax-wabs 172

This theorem is used by: (None)