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

Metamath Proof Explorer

Theorem errel

Description: An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015)

		Ref	Expression
	Assertion	errel	$⊢ R Er A \to Rel R$

Step	Hyp	Ref	Expression
1		df-er	$⊢ R Er A \leftrightarrow (Rel R \land dom R = A \land R^{-1} \cup (R \circ R) \subseteq R)$
2	1	simp1bi	$⊢ R Er A \to Rel R$