Definition df-eqvrels 35862

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 35872. Alternate definitions are dfeqvrels2 35866 and dfeqvrels3 35867. (Contributed by Peter Mazsa, 7-Nov-2018.)

Assertion

Ref	Expression
df-eqvrels	⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

Detailed syntax breakdown of Definition df-eqvrels

Step	Hyp	Ref	Expression
1		ceqvrels 35512	. 2 class EqvRels
2		crefrels 35501	. . . 4 class RefRels
3		csymrels 35507	. . . 4 class SymRels
4	2, 3	cin 3928	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 35510	. . 3 class TrRels
6	4, 5	cin 3928	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1536	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  35866  refrelsredund2  35911