Metamath Proof Explorer

Definition df-trans

Description: Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Assertion df-trans 
|- Trans = ( _V \ ran ( ( _E o. _E ) \ _E ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrans 
 |-  Trans
1 cvv 
 |-  _V
2 cep 
 |-  _E
3 2 2 ccom 
 |-  ( _E o. _E )
4 3 2 cdif 
 |-  ( ( _E o. _E ) \ _E )
5 4 crn 
 |-  ran ( ( _E o. _E ) \ _E )
6 1 5 cdif 
 |-  ( _V \ ran ( ( _E o. _E ) \ _E ) )
7 0 6 wceq 
 |-  Trans = ( _V \ ran ( ( _E o. _E ) \ _E ) )