Definition wrep 163

Description: Type of the representation function.

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
wrep	|- R:(be -> al)

Detailed syntax breakdown of Definition wrep

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

This definition is referenced by: (None)