Definition df-eqvrels 37757

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 37767. Alternate definitions are dfeqvrels2 37761 and dfeqvrels3 37762. (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 37362	. 2 class EqvRels
2		crefrels 37351	. . . 4 class RefRels
3		csymrels 37357	. . . 4 class SymRels
4	2, 3	cin 3946	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 37360	. . 3 class TrRels
6	4, 5	cin 3946	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1539	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  37761  refrelsredund2  37806