Definition df-trans 34138

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

Assertion

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

Detailed syntax breakdown of Definition df-trans

Step	Hyp	Ref	Expression
1		ctrans 34114	. 2 class Trans
2		cvv 3430	. . 3 class V
3		cep 5493	. . . . . 6 class E
4	3, 3	ccom 5592	. . . . 5 class ( E ∘ E )
5	4, 3	cdif 3888	. . . 4 class (( E ∘ E ) ∖ E )
6	5	crn 5589	. . 3 class ran (( E ∘ E ) ∖ E )
7	2, 6	cdif 3888	. 2 class (V ∖ ran (( E ∘ E ) ∖ E ))
8	1, 7	wceq 1541	1 wff Trans = (V ∖ ran (( E ∘ E ) ∖ E ))

This definition is referenced by:  eltrans  34172