Definition df-eqvrels 39050

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 39060. Alternate definitions are dfeqvrels2 39054 and dfeqvrels3 39055. (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 38581	. 2 class EqvRels
2		crefrels 38570	. . . 4 class RefRels
3		csymrels 38576	. . . 4 class SymRels
4	2, 3	cin 3884	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 38579	. . 3 class TrRels
6	4, 5	cin 3884	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1548	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  39054  refrelsredund2  39099