Theorem eqvrelrel

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

	Ref	Expression
Assertion	eqvrelrel	$$⊢EqvRelR\to \mathrm{Rel}R$$

Proof

Step	Hyp	Ref	Expression
1		dfeqvrel2	$$⊢EqvRelR\leftrightarrow \left(\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}R}\subseteq R\wedge R^{-1}\subseteq R\wedge R\circ R\subseteq R\right)\wedge \mathrm{Rel}R\right)$$
2	1	simprbi	$$⊢EqvRelR\to \mathrm{Rel}R$$