Metamath Proof Explorer

Theorem eltrrels2

Description: Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021)

Ref Expression
Assertion eltrrels2 
|- ( R e. TrRels <-> ( ( R o. R ) C_ R /\ R e. Rels ) )

Proof

Step Hyp Ref Expression
1 dftrrels2 
 |-  TrRels = { r e. Rels | ( r o. r ) C_ r }
2 coideq 
 |-  ( r = R -> ( r o. r ) = ( R o. R ) )
3 id 
 |-  ( r = R -> r = R )
4 2 3 sseq12d 
 |-  ( r = R -> ( ( r o. r ) C_ r <-> ( R o. R ) C_ R ) )
5 1 4 rabeqel 
 |-  ( R e. TrRels <-> ( ( R o. R ) C_ R /\ R e. Rels ) )