Metamath Proof Explorer

Theorem cnvimarndm

Description: The preimage of the range of a class is the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009)

Ref Expression
Assertion cnvimarndm 
|- ( `' A " ran A ) = dom A

Proof

Step Hyp Ref Expression
1 imadmrn 
 |-  ( `' A " dom `' A ) = ran `' A
2 df-rn 
 |-  ran A = dom `' A
3 2 imaeq2i 
 |-  ( `' A " ran A ) = ( `' A " dom `' A )
4 dfdm4 
 |-  dom A = ran `' A
5 1 3 4 3eqtr4i 
 |-  ( `' A " ran A ) = dom A