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 Rels | x y z x r y y r z x r z

Proof

Step Hyp Ref Expression
1 dftrrels2 TrRels = r Rels | r r r
2 cotr r r r x y z x r y y r z x r z
3 1 2 rabbieq TrRels = r Rels | x y z x r y y r z x r z