Definition df-eqvrels 38540

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 38550. Alternate definitions are dfeqvrels2 38544 and dfeqvrels3 38545. (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 38151	. 2 class EqvRels
2		crefrels 38140	. . . 4 class RefRels
3		csymrels 38146	. . . 4 class SymRels
4	2, 3	cin 3975	. . 3 class ( RefRels ∩ SymRels )
5		ctrrels 38149	. . 3 class TrRels
6	4, 5	cin 3975	. 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
7	1, 6	wceq 1537	1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

This definition is referenced by:  dfeqvrels2  38544  refrelsredund2  38589