Definition df-eqvrels 39035

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 39045. Alternate definitions are dfeqvrels2 39039 and dfeqvrels3 39040. (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 38566	. 2 class EqvRels
2		crefrels 38555	. . . 4 class RefRels
3		csymrels 38561	. . . 4 class SymRels
4	2, 3	cin 3882	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 38564	. . 3 class TrRels
6	4, 5	cin 3882	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1547	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  39039  refrelsredund2  39084