Definition df-eqvrels 39167

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 39177. Alternate definitions are dfeqvrels2 39171 and dfeqvrels3 39172. (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 38698	. 2 class EqvRels
2		crefrels 38687	. . . 4 class RefRels
3		csymrels 38693	. . . 4 class SymRels
4	2, 3	cin 3903	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 38696	. . 3 class TrRels
6	4, 5	cin 3903	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1560	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  39171  refrelsredund2  39216