Theorem errn

Description: The range and domain of an equivalence relation are equal. (Contributed by Rodolfo Medina, 11-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Assertion	errn	$$⊢R\mathrm{Er}A\to \mathrm{ran}R=A$$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}R=\mathrm{dom}{R}^{-1}$$
2		ercnv	$$⊢R\mathrm{Er}A\to R^{-1}=R$$
3	2	dmeqd	$$⊢R\mathrm{Er}A\to \mathrm{dom}{R}^{-1}=\mathrm{dom}R$$
4		erdm	$$⊢R\mathrm{Er}A\to \mathrm{dom}R=A$$
5	3 4	eqtrd	$$⊢R\mathrm{Er}A\to \mathrm{dom}{R}^{-1}=A$$
6	1 5	syl5eq	$$⊢R\mathrm{Er}A\to \mathrm{ran}R=A$$