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 i^i Rels )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrrels	|- TrRels
1		ctrs	|- Trs
2		crels	|- Rels
3	1 2	cin	|- ( Trs i^i Rels )
4	0 3	wceq	|- TrRels = ( Trs i^i Rels )