Theorem eqvrelrel

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

	Ref	Expression
Assertion	eqvrelrel	⊢ ( EqvRel 𝑅 → Rel 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		dfeqvrel2	⊢ ( EqvRel 𝑅 ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ∧ Rel 𝑅 ) )
2	1	simprbi	⊢ ( EqvRel 𝑅 → Rel 𝑅 )