Definition df-eqvrels 39207

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 39217. Alternate definitions are dfeqvrels2 39211 and dfeqvrels3 39212. (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 38738	. 2 class EqvRels
2		crefrels 38727	. . . 4 class RefRels
3		csymrels 38733	. . . 4 class SymRels
4	2, 3	cin 3912	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 38736	. . 3 class TrRels
6	4, 5	cin 3912	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1567	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  39211  refrelsredund2  39256