Definition df-eqvrels 39866

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 39876. Alternate definitions are dfeqvrels2 39870 and dfeqvrels3 39871. (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 39397	. 2 class EqvRels
2		crefrels 39386	. . . 4 class RefRels
3		csymrels 39392	. . . 4 class SymRels
4	2, 3	cin 4092	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 39395	. . 3 class TrRels
6	4, 5	cin 4092	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1570	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is used by:  dfeqvrels2  39870  refrelsredund2  39915