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 Er A -> ran R = A )

Proof

Step	Hyp	Ref	Expression
1		df-rn	|- ran R = dom `' R
2		ercnv	|- ( R Er A -> `' R = R )
3	2	dmeqd	|- ( R Er A -> dom `' R = dom R )
4		erdm	|- ( R Er A -> dom R = A )
5	3 4	eqtrd	|- ( R Er A -> dom `' R = A )
6	1 5	eqtrid	|- ( R Er A -> ran R = A )