Definition df-eqvrels 37449

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 37459. Alternate definitions are dfeqvrels2 37453 and dfeqvrels3 37454. (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 37054	. 2 class EqvRels
2		crefrels 37043	. . . 4 class RefRels
3		csymrels 37049	. . . 4 class SymRels
4	2, 3	cin 3947	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 37052	. . 3 class TrRels
6	4, 5	cin 3947	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1541	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  37453  refrelsredund2  37498