Definition df-eqvrels 39337

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 39347. Alternate definitions are dfeqvrels2 39341 and dfeqvrels3 39342. (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 38868	. 2 class EqvRels
2		crefrels 38857	. . . 4 class RefRels
3		csymrels 38863	. . . 4 class SymRels
4	2, 3	cin 3904	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 38866	. . 3 class TrRels
6	4, 5	cin 3904	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1570	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  39341  refrelsredund2  39386