Definition df-tcfn 6108

Description: Define the stratified T-raising function. (Contributed by Scott Fenton, 24-Feb-2015.)

Assertion

Ref	Expression
df-tcfn	⊢ TcFn = (x ∈ 1c ↦ Tc ∪x)

Detailed syntax breakdown of Definition df-tcfn

Step	Hyp	Ref	Expression
1		ctcfn 6098	. 2 class TcFn
2		vx	. . 3 setvar x
3		c1c 4135	. . 3 class 1c
4	2	cv 1641	. . . . 5 class x
5	4	cuni 3892	. . . 4 class ∪x
6	5	ctc 6094	. . 3 class Tc ∪x
7	2, 3, 6	cmpt 5652	. 2 class (x ∈ 1c ↦ Tc ∪x)
8	1, 7	wceq 1642	1 wff TcFn = (x ∈ 1c ↦ Tc ∪x)

This definition is referenced by:  tcfnex  6245  fntcfn  6246  brtcfn  6247