Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-trans Structured version   Visualization version   GIF version

Definition df-trans 33215
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
StepHypRef Expression
1 ctrans 33191 . 2 class Trans
2 cvv 3492 . . 3 class V
3 cep 5457 . . . . . 6 class E
43, 3ccom 5552 . . . . 5 class ( E ∘ E )
54, 3cdif 3930 . . . 4 class (( E ∘ E ) ∖ E )
65crn 5549 . . 3 class ran (( E ∘ E ) ∖ E )
72, 6cdif 3930 . 2 class (V ∖ ran (( E ∘ E ) ∖ E ))
81, 7wceq 1528 1 wff Trans = (V ∖ ran (( E ∘ E ) ∖ E ))
Colors of variables: wff setvar class
This definition is referenced by:  eltrans  33249
  Copyright terms: Public domain W3C validator