Definition df-eqvrels

Description: Define the class of equivalence relations. For sets, being an element of the class of equivalence relations is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel . Alternate definitions are dfeqvrels2 and dfeqvrels3 . (Contributed by Peter Mazsa, 7-Nov-2018)

	Ref	Expression
Assertion	df-eqvrels	|- EqvRels = ( ( RefRels i^i SymRels ) i^i TrRels )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceqvrels	|- EqvRels
1		crefrels	|- RefRels
2		csymrels	|- SymRels
3	1 2	cin	|- ( RefRels i^i SymRels )
4		ctrrels	|- TrRels
5	3 4	cin	|- ( ( RefRels i^i SymRels ) i^i TrRels )
6	0 5	wceq	|- EqvRels = ( ( RefRels i^i SymRels ) i^i TrRels )