Theorem eqvrelim

Description: Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021)

	Ref	Expression
Assertion	eqvrelim	⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		eqvrelsymrel	⊢ ( EqvRel 𝑅 → SymRel 𝑅 )
2		symrelim	⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅 )
3	1 2	syl	⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅 )