Definition df-eqvrels 39740

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 39750. Alternate definitions are dfeqvrels2 39744 and dfeqvrels3 39745. (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 39271	. 2 class EqvRels
2		crefrels 39260	. . . 4 class RefRels
3		csymrels 39266	. . . 4 class SymRels
4	2, 3	cin 4091	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 39269	. . 3 class TrRels
6	4, 5	cin 4091	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1569	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is used by:  dfeqvrels2  39744  refrelsredund2  39789