# Metamath Proof Explorer

## Theorem dfima2

Description: Alternate definition of image. Compare definition (d) of Enderton p. 44. (Contributed by NM, 19-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfima2 ${⊢}{A}\left[{B}\right]=\left\{{y}|\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}$

### Proof

Step Hyp Ref Expression
1 df-ima ${⊢}{A}\left[{B}\right]=\mathrm{ran}\left({{A}↾}_{{B}}\right)$
2 dfrn2 ${⊢}\mathrm{ran}\left({{A}↾}_{{B}}\right)=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{x}\left({{A}↾}_{{B}}\right){y}\right\}$
3 brres ${⊢}{y}\in \mathrm{V}\to \left({x}\left({{A}↾}_{{B}}\right){y}↔\left({x}\in {B}\wedge {x}{A}{y}\right)\right)$
4 3 elv ${⊢}{x}\left({{A}↾}_{{B}}\right){y}↔\left({x}\in {B}\wedge {x}{A}{y}\right)$
5 4 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}\left({{A}↾}_{{B}}\right){y}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {x}{A}{y}\right)$
6 df-rex ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {x}{A}{y}\right)$
7 5 6 bitr4i ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}\left({{A}↾}_{{B}}\right){y}↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$
8 7 abbii ${⊢}\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{x}\left({{A}↾}_{{B}}\right){y}\right\}=\left\{{y}|\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}$
9 1 2 8 3eqtri ${⊢}{A}\left[{B}\right]=\left\{{y}|\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}$