This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union Equivalence relations and classes 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
eqtrid ⊢ ( 𝑅 Er 𝐴 → ran 𝑅 = 𝐴 )