Metamath Proof Explorer

Theorem imadmrn

Description: The image of the domain of a class is equal to its range. (Contributed by NM, 14-Aug-1994) (Proof shortened by BJ, 27-Sep-2026)

Ref Expression
Assertion imadmrn 
|- ( A " dom A ) = ran A

Proof

Step Hyp Ref Expression
1 ssid 
 |-  dom A C_ dom A
2 dfrn7 
 |-  ( dom A C_ dom A -> ran A = ( A " dom A ) )
3 2 eqcomd 
 |-  ( dom A C_ dom A -> ( A " dom A ) = ran A )
4 1 3 ax-mp 
 |-  ( A " dom A ) = ran A