Definition df-eqvrels 35834

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 35844. Alternate definitions are dfeqvrels2 35838 and dfeqvrels3 35839. (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 35484	. 2 class EqvRels
2		crefrels 35473	. . . 4 class RefRels
3		csymrels 35479	. . . 4 class SymRels
4	2, 3	cin 3935	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 35482	. . 3 class TrRels
6	4, 5	cin 3935	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1537	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  35838  refrelsredund2  35883