Metamath Proof Explorer

Theorem cnvimarndm

Description: The preimage of the range of a class is equal to the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009) (Proof shortened by BJ, 29-Sep-2026)

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

Proof

Step Hyp Ref Expression
1 ssid 
 |-  ran A C_ ran A
2 cnvimassrndm 
 |-  ( ran A C_ ran A -> ( `' A " ran A ) = dom A )
3 1 2 ax-mp 
 |-  ( `' A " ran A ) = dom A