Definition df-eqvrels 39377

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 39387. Alternate definitions are dfeqvrels2 39381 and dfeqvrels3 39382. (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 38908	. 2 class EqvRels
2		crefrels 38897	. . . 4 class RefRels
3		csymrels 38903	. . . 4 class SymRels
4	2, 3	cin 3905	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 38906	. . 3 class TrRels
6	4, 5	cin 3905	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1570	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is used by:  dfeqvrels2  39381  refrelsredund2  39426