Definition df-eqvrels

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 . Alternate definitions are dfeqvrels2 and dfeqvrels3 . (Contributed by Peter Mazsa, 7-Nov-2018)

	Ref	Expression
Assertion	df-eqvrels	$$⊢\mathrm{EqvRels}=\left(\mathrm{RefRels}\cap \mathrm{SymRels}\right)\cap \mathrm{TrRels}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceqvrels	$$class\mathrm{EqvRels}$$
1		crefrels	$$class\mathrm{RefRels}$$
2		csymrels	$$class\mathrm{SymRels}$$
3	1 2	cin	$$class\left(\mathrm{RefRels}\cap \mathrm{SymRels}\right)$$
4		ctrrels	$$class\mathrm{TrRels}$$
5	3 4	cin	$$class\left(\left(\mathrm{RefRels}\cap \mathrm{SymRels}\right)\cap \mathrm{TrRels}\right)$$
6	0 5	wceq	$$wff\mathrm{EqvRels}=\left(\mathrm{RefRels}\cap \mathrm{SymRels}\right)\cap \mathrm{TrRels}$$