Axiom ax-wrep 173

Description: Type of the representation function. (New usage is discouraged.) (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
ax-wrep	⊢ R:(β → α)

Detailed syntax breakdown of Axiom ax-wrep

Step	Hyp	Ref	Expression
1		hbe	. . 3 type β
2		hal	. . 3 type α
3	1, 2	ht 2	. 2 type (β → α)
4		tr	. 2 term R
5	3, 4	wffMMJ2t 12	1 wff R:(β → α)

This axiom is referenced by:  wrep  175