Description: Range defined in terms of image. (Contributed by NM, 14-May-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | dfrn4 | ⊢ ran 𝐴 = ( 𝐴 “ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ima | ⊢ ( 𝐴 “ V ) = ran ( 𝐴 ↾ V ) | |
2 | rnresv | ⊢ ran ( 𝐴 ↾ V ) = ran 𝐴 | |
3 | 1 2 | eqtr2i | ⊢ ran 𝐴 = ( 𝐴 “ V ) |