# Metamath Proof Explorer

## Theorem funimass4f

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017)

Ref Expression
Hypotheses funimass4f.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
funimass4f.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
funimass4f.3 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
Assertion funimass4f ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left({F}\left[{A}\right]\subseteq {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$

### Proof

Step Hyp Ref Expression
1 funimass4f.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 funimass4f.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 funimass4f.3 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
4 3 nffun ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{F}$
5 3 nfdm ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}$
6 1 5 nfss ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\subseteq \mathrm{dom}{F}$
7 4 6 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)$
8 3 1 nfima ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left[{A}\right]$
9 8 2 nfss ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}\left[{A}\right]\subseteq {B}$
10 7 9 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\wedge {F}\left[{A}\right]\subseteq {B}\right)$
11 funfvima2 ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left({x}\in {A}\to {F}\left({x}\right)\in {F}\left[{A}\right]\right)$
12 ssel ${⊢}{F}\left[{A}\right]\subseteq {B}\to \left({F}\left({x}\right)\in {F}\left[{A}\right]\to {F}\left({x}\right)\in {B}\right)$
13 11 12 sylan9 ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\wedge {F}\left[{A}\right]\subseteq {B}\right)\to \left({x}\in {A}\to {F}\left({x}\right)\in {B}\right)$
14 10 13 ralrimi ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\wedge {F}\left[{A}\right]\subseteq {B}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}$
15 1 3 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\}$
16 15 adantr ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)\to {F}\left[{A}\right]=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}$
17 2 abrexss ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\to \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}\subseteq {B}$
18 17 adantl ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)\to \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}\subseteq {B}$
19 16 18 eqsstrd ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)\to {F}\left[{A}\right]\subseteq {B}$
20 14 19 impbida ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left({F}\left[{A}\right]\subseteq {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$