Definition df-trans

Description: Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	df-trans	$$⊢\mathrm{𝖳𝗋𝖺𝗇𝗌}=\mathrm{V}\setminus \mathrm{ran}\left(\left(\mathrm{E}\circ \mathrm{E}\right)\setminus \mathrm{E}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrans	$$class\mathrm{𝖳𝗋𝖺𝗇𝗌}$$
1		cvv	$$class\mathrm{V}$$
2		cep	$$class\mathrm{E}$$
3	2 2	ccom	$$class\left(\mathrm{E}\circ \mathrm{E}\right)$$
4	3 2	cdif	$$class\left(\left(\mathrm{E}\circ \mathrm{E}\right)\setminus \mathrm{E}\right)$$
5	4	crn	$$class\mathrm{ran}\left(\left(\mathrm{E}\circ \mathrm{E}\right)\setminus \mathrm{E}\right)$$
6	1 5	cdif	$$class\left(\mathrm{V}\setminus \mathrm{ran}\left(\left(\mathrm{E}\circ \mathrm{E}\right)\setminus \mathrm{E}\right)\right)$$
7	0 6	wceq	$$wff\mathrm{𝖳𝗋𝖺𝗇𝗌}=\mathrm{V}\setminus \mathrm{ran}\left(\left(\mathrm{E}\circ \mathrm{E}\right)\setminus \mathrm{E}\right)$$