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

Metamath Proof Explorer

Theorem eqvrelrel

Description: An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019)

		Ref	Expression
	Assertion	eqvrelrel	$⊢ EqvRel R \to Rel R$

Step	Hyp	Ref	Expression
1		dfeqvrel2	$⊢ EqvRel R \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land Rel R)$
2	1	simprbi	$⊢ EqvRel R \to Rel R$