Definition df-trans

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

	Ref	Expression
Assertion	df-trans	⊢ Trans = ( V ∖ ran ( ( E ∘ E ) ∖ E ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrans	⊢ Trans
1		cvv	⊢ V
2		cep	⊢ E
3	2 2	ccom	⊢ ( E ∘ E )
4	3 2	cdif	⊢ ( ( E ∘ E ) ∖ E )
5	4	crn	⊢ ran ( ( E ∘ E ) ∖ E )
6	1 5	cdif	⊢ ( V ∖ ran ( ( E ∘ E ) ∖ E ) )
7	0 6	wceq	⊢ Trans = ( V ∖ ran ( ( E ∘ E ) ∖ E ) )