Definition df-eqvrels 38548

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 38558. Alternate definitions are dfeqvrels2 38552 and dfeqvrels3 38553. (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 38161	. 2 class EqvRels
2		crefrels 38150	. . . 4 class RefRels
3		csymrels 38156	. . . 4 class SymRels
4	2, 3	cin 3925	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 38159	. . 3 class TrRels
6	4, 5	cin 3925	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1540	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  38552  refrelsredund2  38597