Metamath Proof Explorer


Definition df-trrels

Description: Define the class of transitive relations. For sets, being an element of the class of transitive relations is equivalent to satisfying the transitive relation predicate, see eltrrelsrel . Alternate definitions are dftrrels2 and dftrrels3 .

This definition is similar to the definitions of the classes of reflexive ( df-refrels ) and symmetric ( df-symrels ) relations. (Contributed by Peter Mazsa, 7-Jul-2019)

Ref Expression
Assertion df-trrels TrRels = Trs Rels

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrrels class TrRels
1 ctrs class Trs
2 crels class Rels
3 1 2 cin class Trs Rels
4 0 3 wceq wff TrRels = Trs Rels