Definition df-eqvrels 38045

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 38055. Alternate definitions are dfeqvrels2 38049 and dfeqvrels3 38050. (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 37653	. 2 class EqvRels
2		crefrels 37642	. . . 4 class RefRels
3		csymrels 37648	. . . 4 class SymRels
4	2, 3	cin 3943	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 37651	. . 3 class TrRels
6	4, 5	cin 3943	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1534	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  38049  refrelsredund2  38094