Metamath Proof Explorer

Theorem funimass4

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion funimass4 ${⊢}\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 dfss2 ${⊢}{F}\left[{A}\right]\subseteq {B}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {F}\left[{A}\right]\to {y}\in {B}\right)$
2 eqcom ${⊢}{y}={F}\left({x}\right)↔{F}\left({x}\right)={y}$
3 ssel ${⊢}{A}\subseteq \mathrm{dom}{F}\to \left({x}\in {A}\to {x}\in \mathrm{dom}{F}\right)$
4 funbrfvb ${⊢}\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)\to \left({F}\left({x}\right)={y}↔{x}{F}{y}\right)$
5 4 ex ${⊢}\mathrm{Fun}{F}\to \left({x}\in \mathrm{dom}{F}\to \left({F}\left({x}\right)={y}↔{x}{F}{y}\right)\right)$
6 3 5 syl9 ${⊢}{A}\subseteq \mathrm{dom}{F}\to \left(\mathrm{Fun}{F}\to \left({x}\in {A}\to \left({F}\left({x}\right)={y}↔{x}{F}{y}\right)\right)\right)$
7 6 imp31 ${⊢}\left(\left({A}\subseteq \mathrm{dom}{F}\wedge \mathrm{Fun}{F}\right)\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)={y}↔{x}{F}{y}\right)$
8 2 7 syl5bb ${⊢}\left(\left({A}\subseteq \mathrm{dom}{F}\wedge \mathrm{Fun}{F}\right)\wedge {x}\in {A}\right)\to \left({y}={F}\left({x}\right)↔{x}{F}{y}\right)$
9 8 rexbidva ${⊢}\left({A}\subseteq \mathrm{dom}{F}\wedge \mathrm{Fun}{F}\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)$
10 vex ${⊢}{y}\in \mathrm{V}$
11 10 elima ${⊢}{y}\in {F}\left[{A}\right]↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}{F}{y}$
12 9 11 syl6rbbr ${⊢}\left({A}\subseteq \mathrm{dom}{F}\wedge \mathrm{Fun}{F}\right)\to \left({y}\in {F}\left[{A}\right]↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)$
13 12 imbi1d ${⊢}\left({A}\subseteq \mathrm{dom}{F}\wedge \mathrm{Fun}{F}\right)\to \left(\left({y}\in {F}\left[{A}\right]\to {y}\in {B}\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\to {y}\in {B}\right)\right)$
14 r19.23v ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}={F}\left({x}\right)\to {y}\in {B}\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\to {y}\in {B}\right)$
15 13 14 syl6bbr ${⊢}\left({A}\subseteq \mathrm{dom}{F}\wedge \mathrm{Fun}{F}\right)\to \left(\left({y}\in {F}\left[{A}\right]\to {y}\in {B}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}={F}\left({x}\right)\to {y}\in {B}\right)\right)$
16 15 albidv ${⊢}\left({A}\subseteq \mathrm{dom}{F}\wedge \mathrm{Fun}{F}\right)\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {F}\left[{A}\right]\to {y}\in {B}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}={F}\left({x}\right)\to {y}\in {B}\right)\right)$
17 ralcom4 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={F}\left({x}\right)\to {y}\in {B}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}={F}\left({x}\right)\to {y}\in {B}\right)$
18 fvex ${⊢}{F}\left({x}\right)\in \mathrm{V}$
19 eleq1 ${⊢}{y}={F}\left({x}\right)\to \left({y}\in {B}↔{F}\left({x}\right)\in {B}\right)$
20 18 19 ceqsalv ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={F}\left({x}\right)\to {y}\in {B}\right)↔{F}\left({x}\right)\in {B}$
21 20 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={F}\left({x}\right)\to {y}\in {B}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}$
22 17 21 bitr3i ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}={F}\left({x}\right)\to {y}\in {B}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}$
23 16 22 syl6bb ${⊢}\left({A}\subseteq \mathrm{dom}{F}\wedge \mathrm{Fun}{F}\right)\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {F}\left[{A}\right]\to {y}\in {B}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$
24 1 23 syl5bb ${⊢}\left({A}\subseteq \mathrm{dom}{F}\wedge \mathrm{Fun}{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)$
25 24 ancoms ${⊢}\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)$