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	⊢ ( 𝑅 Er 𝐴 → ran 𝑅 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran 𝑅 = dom ◡ 𝑅
2		ercnv	⊢ ( 𝑅 Er 𝐴 → ◡ 𝑅 = 𝑅 )
3	2	dmeqd	⊢ ( 𝑅 Er 𝐴 → dom ◡ 𝑅 = dom 𝑅 )
4		erdm	⊢ ( 𝑅 Er 𝐴 → dom 𝑅 = 𝐴 )
5	3 4	eqtrd	⊢ ( 𝑅 Er 𝐴 → dom ◡ 𝑅 = 𝐴 )
6	1 5	syl5eq	⊢ ( 𝑅 Er 𝐴 → ran 𝑅 = 𝐴 )