Metamath Proof Explorer


Theorem dfrn4

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

Ref Expression
Assertion dfrn4 ran 𝐴 = ( 𝐴 “ V )

Proof

Step Hyp Ref Expression
1 df-ima ( 𝐴 “ V ) = ran ( 𝐴 ↾ V )
2 rnresv ran ( 𝐴 ↾ V ) = ran 𝐴
3 1 2 eqtr2i ran 𝐴 = ( 𝐴 “ V )