Definition df-eqvrels 37758

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 37768. Alternate definitions are dfeqvrels2 37762 and dfeqvrels3 37763. (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 37363	. 2 class EqvRels
2		crefrels 37352	. . . 4 class RefRels
3		csymrels 37358	. . . 4 class SymRels
4	2, 3	cin 3948	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 37361	. . 3 class TrRels
6	4, 5	cin 3948	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1540	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  37762  refrelsredund2  37807