Metamath Proof Explorer

Theorem dftrrels3

Description: Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021)

Ref Expression
Assertion dftrrels3 
|- TrRels = { r e. Rels | A. x A. y A. z ( ( x r y /\ y r z ) -> x r z ) }

Proof

Step Hyp Ref Expression
1 dftrrels2 
 |-  TrRels = { r e. Rels | ( r o. r ) C_ r }
2 cotr 
 |-  ( ( r o. r ) C_ r <-> A. x A. y A. z ( ( x r y /\ y r z ) -> x r z ) )
3 1 2 rabbieq 
 |-  TrRels = { r e. Rels | A. x A. y A. z ( ( x r y /\ y r z ) -> x r z ) }