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

Metamath Proof Explorer

Definition df-eqvrel

Description: Define the equivalence relation predicate. (Read: R is an equivalence relation.) For sets, being an element of the class of equivalence relations ( df-eqvrels ) is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel . Alternate definitions are dfeqvrel2 and dfeqvrel3 . (Contributed by Peter Mazsa, 17-Apr-2019)

		Ref	Expression
	Assertion	df-eqvrel	$⊢ EqvRel R \leftrightarrow (RefRel R \land SymRel R \land TrRel R)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1	0	weqvrel	$wff EqvRel R$
2	0	wrefrel	$wff RefRel R$
3	0	wsymrel	$wff SymRel R$
4	0	wtrrel	$wff TrRel R$
5	2 3 4	w3a	$wff (RefRel R \land SymRel R \land TrRel R)$
6	1 5	wb	$wff (EqvRel R \leftrightarrow (RefRel R \land SymRel R \land TrRel R))$