Definition df-trrels 35852

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 35860. Alternate definitions are dftrrels2 35854 and dftrrels3 35855.

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

Assertion

Ref	Expression
df-trrels	⊢ TrRels = ( Trs ∩ Rels )

Detailed syntax breakdown of Definition df-trrels

Step	Hyp	Ref	Expression
1		ctrrels 35510	. 2 class TrRels
2		ctrs 35509	. . 3 class Trs
3		crels 35498	. . 3 class Rels
4	2, 3	cin 3928	. 2 class ( Trs ∩ Rels )
5	1, 4	wceq 1536	1 wff TrRels = ( Trs ∩ Rels )

This definition is referenced by:  dftrrels2  35854