Metamath Proof Explorer


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 RErAranR=A

Proof

Step Hyp Ref Expression
1 df-rn ranR=domR-1
2 ercnv RErAR-1=R
3 2 dmeqd RErAdomR-1=domR
4 erdm RErAdomR=A
5 3 4 eqtrd RErAdomR-1=A
6 1 5 eqtrid RErAranR=A