Definition df-eqvrels 39006

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 39016. Alternate definitions are dfeqvrels2 39010 and dfeqvrels3 39011. (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 38537	. 2 class EqvRels
2		crefrels 38526	. . . 4 class RefRels
3		csymrels 38532	. . . 4 class SymRels
4	2, 3	cin 3889	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 38535	. . 3 class TrRels
6	4, 5	cin 3889	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1542	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  39010  refrelsredund2  39055