Metamath Proof Explorer

Theorem dfrn4

Description: Range defined in terms of image. (Contributed by NM, 14-May-2008)

Ref Expression
Assertion dfrn4 
|- ran A = ( A " _V )

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( A " _V ) = ran ( A |` _V )
2 rnresv 
 |-  ran ( A |` _V ) = ran A
3 1 2 eqtr2i 
 |-  ran A = ( A " _V )