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

Definition df-trans 24398
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 24376 . 2  class  Trans
2 cvv 2788 . . 3  class  _V
3 cep 4303 . . . . . 6  class  _E
43, 3ccom 4693 . . . . 5  class  (  _E  o.  _E  )
54, 3cdif 3149 . . . 4  class  ( (  _E  o.  _E  )  \  _E  )
65crn 4690 . . 3  class  ran  (
(  _E  o.  _E  )  \  _E  )
72, 6cdif 3149 . 2  class  ( _V 
\  ran  ( (  _E  o.  _E  )  \  _E  ) )
81, 7wceq 1623 1  wff  Trans  =  ( _V  \  ran  (
(  _E  o.  _E  )  \  _E  ) )
Colors of variables: wff set class
This definition is referenced by:  eltrans  24431
  Copyright terms: Public domain W3C validator