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