Definition df-eqvrels 38851

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 38861. Alternate definitions are dfeqvrels2 38855 and dfeqvrels3 38856. (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 38399	. 2 class EqvRels
2		crefrels 38388	. . . 4 class RefRels
3		csymrels 38394	. . . 4 class SymRels
4	2, 3	cin 3900	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 38397	. . 3 class TrRels
6	4, 5	cin 3900	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1541	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  38855  refrelsredund2  38900