Definition df-eqvrels 36624

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 36634. Alternate definitions are dfeqvrels2 36628 and dfeqvrels3 36629. (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 36276	. 2 class EqvRels
2		crefrels 36265	. . . 4 class RefRels
3		csymrels 36271	. . . 4 class SymRels
4	2, 3	cin 3882	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 36274	. . 3 class TrRels
6	4, 5	cin 3882	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1539	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  36628  refrelsredund2  36673