This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ EqvRels = (RefRels \cap SymRels) \cap TrRels$

Detailed syntax breakdown

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