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 35352
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 35328 . 2 class Trans
2 cvv 3466 . . 3 class V
3 cep 5570 . . . . . 6 class E
43, 3ccom 5671 . . . . 5 class ( E ∘ E )
54, 3cdif 3938 . . . 4 class (( E ∘ E ) ∖ E )
65crn 5668 . . 3 class ran (( E ∘ E ) ∖ E )
72, 6cdif 3938 . 2 class (V ∖ ran (( E ∘ E ) ∖ E ))
81, 7wceq 1533 1 wff Trans = (V ∖ ran (( E ∘ E ) ∖ E ))
Colors of variables: wff setvar class
This definition is referenced by:  eltrans  35386
  Copyright terms: Public domain W3C validator