Description: Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | df-trans |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ctrans | ||
1 | cvv | ||
2 | cep | ||
3 | 2 2 | ccom | |
4 | 3 2 | cdif | |
5 | 4 | crn | |
6 | 1 5 | cdif | |
7 | 0 6 | wceq |