Definition df-eqvrels 38989

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 38999. Alternate definitions are dfeqvrels2 38993 and dfeqvrels3 38994. (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 38520	. 2 class EqvRels
2		crefrels 38509	. . . 4 class RefRels
3		csymrels 38515	. . . 4 class SymRels
4	2, 3	cin 3888	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 38518	. . 3 class TrRels
6	4, 5	cin 3888	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1542	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  38993  refrelsredund2  39038