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 32298
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 32274 . 2 class Trans
2 cvv 3351 . . 3 class V
3 cep 5161 . . . . . 6 class E
43, 3ccom 5253 . . . . 5 class ( E ∘ E )
54, 3cdif 3720 . . . 4 class (( E ∘ E ) ∖ E )
65crn 5250 . . 3 class ran (( E ∘ E ) ∖ E )
72, 6cdif 3720 . 2 class (V ∖ ran (( E ∘ E ) ∖ E ))
81, 7wceq 1631 1 wff Trans = (V ∖ ran (( E ∘ E ) ∖ E ))
Colors of variables: wff setvar class
This definition is referenced by:  eltrans  32332
  Copyright terms: Public domain W3C validator