# Metamath Proof Explorer

## Theorem dfimafnf

Description: Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006) (Revised by Thierry Arnoux, 24-Apr-2017)

Ref Expression
Hypotheses dfimafnf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
dfimafnf.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
Assertion dfimafnf ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to {F}\left[{A}\right]=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 dfimafnf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 dfimafnf.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
3 ssel ${⊢}{A}\subseteq \mathrm{dom}{F}\to \left({z}\in {A}\to {z}\in \mathrm{dom}{F}\right)$
4 eqcom ${⊢}{F}\left({z}\right)={y}↔{y}={F}\left({z}\right)$
5 funbrfvb ${⊢}\left(\mathrm{Fun}{F}\wedge {z}\in \mathrm{dom}{F}\right)\to \left({F}\left({z}\right)={y}↔{z}{F}{y}\right)$
6 4 5 syl5bbr ${⊢}\left(\mathrm{Fun}{F}\wedge {z}\in \mathrm{dom}{F}\right)\to \left({y}={F}\left({z}\right)↔{z}{F}{y}\right)$
7 6 ex ${⊢}\mathrm{Fun}{F}\to \left({z}\in \mathrm{dom}{F}\to \left({y}={F}\left({z}\right)↔{z}{F}{y}\right)\right)$
8 3 7 syl9r ${⊢}\mathrm{Fun}{F}\to \left({A}\subseteq \mathrm{dom}{F}\to \left({z}\in {A}\to \left({y}={F}\left({z}\right)↔{z}{F}{y}\right)\right)\right)$
9 8 imp31 ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\wedge {z}\in {A}\right)\to \left({y}={F}\left({z}\right)↔{z}{F}{y}\right)$
10 9 rexbidva ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left(\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({z}\right)↔\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{F}{y}\right)$
11 10 abbidv ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left\{{y}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({z}\right)\right\}=\left\{{y}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{F}{y}\right\}$
12 dfima2 ${⊢}{F}\left[{A}\right]=\left\{{y}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{F}{y}\right\}$
13 11 12 syl6reqr ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to {F}\left[{A}\right]=\left\{{y}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({z}\right)\right\}$
14 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{A}$
15 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
16 2 15 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)$
17 16 nfeq2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}={F}\left({z}\right)$
18 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)$
19 fveq2 ${⊢}{z}={x}\to {F}\left({z}\right)={F}\left({x}\right)$
20 19 eqeq2d ${⊢}{z}={x}\to \left({y}={F}\left({z}\right)↔{y}={F}\left({x}\right)\right)$
21 14 1 17 18 20 cbvrexfw ${⊢}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({z}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)$
22 21 abbii ${⊢}\left\{{y}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({z}\right)\right\}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}$
23 13 22 syl6eq ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to {F}\left[{A}\right]=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}$