# Metamath Proof Explorer

## Theorem fvimacnvi

Description: A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007)

Ref Expression
Assertion fvimacnvi ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in {{F}}^{-1}\left[{B}\right]\right)\to {F}\left({A}\right)\in {B}$

### Proof

Step Hyp Ref Expression
1 snssi ${⊢}{A}\in {{F}}^{-1}\left[{B}\right]\to \left\{{A}\right\}\subseteq {{F}}^{-1}\left[{B}\right]$
2 funimass2 ${⊢}\left(\mathrm{Fun}{F}\wedge \left\{{A}\right\}\subseteq {{F}}^{-1}\left[{B}\right]\right)\to {F}\left[\left\{{A}\right\}\right]\subseteq {B}$
3 1 2 sylan2 ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in {{F}}^{-1}\left[{B}\right]\right)\to {F}\left[\left\{{A}\right\}\right]\subseteq {B}$
4 fvex ${⊢}{F}\left({A}\right)\in \mathrm{V}$
5 4 snss ${⊢}{F}\left({A}\right)\in {B}↔\left\{{F}\left({A}\right)\right\}\subseteq {B}$
6 cnvimass ${⊢}{{F}}^{-1}\left[{B}\right]\subseteq \mathrm{dom}{F}$
7 6 sseli ${⊢}{A}\in {{F}}^{-1}\left[{B}\right]\to {A}\in \mathrm{dom}{F}$
8 funfn ${⊢}\mathrm{Fun}{F}↔{F}Fn\mathrm{dom}{F}$
9 fnsnfv ${⊢}\left({F}Fn\mathrm{dom}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to \left\{{F}\left({A}\right)\right\}={F}\left[\left\{{A}\right\}\right]$
10 8 9 sylanb ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to \left\{{F}\left({A}\right)\right\}={F}\left[\left\{{A}\right\}\right]$
11 7 10 sylan2 ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in {{F}}^{-1}\left[{B}\right]\right)\to \left\{{F}\left({A}\right)\right\}={F}\left[\left\{{A}\right\}\right]$
12 11 sseq1d ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in {{F}}^{-1}\left[{B}\right]\right)\to \left(\left\{{F}\left({A}\right)\right\}\subseteq {B}↔{F}\left[\left\{{A}\right\}\right]\subseteq {B}\right)$
13 5 12 syl5bb ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in {{F}}^{-1}\left[{B}\right]\right)\to \left({F}\left({A}\right)\in {B}↔{F}\left[\left\{{A}\right\}\right]\subseteq {B}\right)$
14 3 13 mpbird ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in {{F}}^{-1}\left[{B}\right]\right)\to {F}\left({A}\right)\in {B}$