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

Definition df-trans 25620
Description: Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
Assertion
Ref Expression
df-trans  |-  Trans  =  ( _V  \  ran  (
(  _E  o.  _E  )  \  _E  ) )

Detailed syntax breakdown of Definition df-trans
StepHypRef Expression
1 ctrans 25598 . 2  class  Trans
2 cvv 2924 . . 3  class  _V
3 cep 4460 . . . . . 6  class  _E
43, 3ccom 4849 . . . . 5  class  (  _E  o.  _E  )
54, 3cdif 3285 . . . 4  class  ( (  _E  o.  _E  )  \  _E  )
65crn 4846 . . 3  class  ran  (
(  _E  o.  _E  )  \  _E  )
72, 6cdif 3285 . 2  class  ( _V 
\  ran  ( (  _E  o.  _E  )  \  _E  ) )
81, 7wceq 1649 1  wff  Trans  =  ( _V  \  ran  (
(  _E  o.  _E  )  \  _E  ) )
Colors of variables: wff set class
This definition is referenced by:  eltrans  25653
  Copyright terms: Public domain W3C validator