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	$$⊢EqvRelR\to \mathrm{dom}R=\mathrm{ran}R$$

Proof

Step	Hyp	Ref	Expression
1		eqvrelsymrel	$$⊢EqvRelR\to SymRelR$$
2		symrelim	$$⊢SymRelR\to \mathrm{dom}R=\mathrm{ran}R$$
3	1 2	syl	$$⊢EqvRelR\to \mathrm{dom}R=\mathrm{ran}R$$