Description: The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | trin | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin | |
|
2 | trss | |
|
3 | trss | |
|
4 | 2 3 | im2anan9 | |
5 | 1 4 | syl5bi | |
6 | ssin | |
|
7 | 5 6 | syl6ib | |
8 | 7 | ralrimiv | |
9 | dftr3 | |
|
10 | 8 9 | sylibr | |