Definition df-tc

Description: The transitive closure function. (Contributed by Mario Carneiro, 23-Jun-2013)

	Ref	Expression
Assertion	df-tc	$$⊢\mathrm{TC}=\left(x\in \mathrm{V}⟼\bigcap \left\{y|\left(x\subseteq y\wedge \mathrm{Tr}y\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctc	$$class\mathrm{TC}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5	3	cv	$$setvary$$
6	4 5	wss	$$wffx\subseteq y$$
7	5	wtr	$$wff\mathrm{Tr}y$$
8	6 7	wa	$$wff\left(x\subseteq y\wedge \mathrm{Tr}y\right)$$
9	8 3	cab	$$class\left\{y|\left(x\subseteq y\wedge \mathrm{Tr}y\right)\right\}$$
10	9	cint	$$class\bigcap \left\{y|\left(x\subseteq y\wedge \mathrm{Tr}y\right)\right\}$$
11	1 2 10	cmpt	$$class\left(x\in \mathrm{V}⟼\bigcap \left\{y|\left(x\subseteq y\wedge \mathrm{Tr}y\right)\right\}\right)$$
12	0 11	wceq	$$wff\mathrm{TC}=\left(x\in \mathrm{V}⟼\bigcap \left\{y|\left(x\subseteq y\wedge \mathrm{Tr}y\right)\right\}\right)$$