# Metamath Proof Explorer

## Theorem elpreima

Description: Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion elpreima ${⊢}{F}Fn{A}\to \left({B}\in {{F}}^{-1}\left[{C}\right]↔\left({B}\in {A}\wedge {F}\left({B}\right)\in {C}\right)\right)$

### Proof

Step Hyp Ref Expression
1 cnvimass ${⊢}{{F}}^{-1}\left[{C}\right]\subseteq \mathrm{dom}{F}$
2 1 sseli ${⊢}{B}\in {{F}}^{-1}\left[{C}\right]\to {B}\in \mathrm{dom}{F}$
3 fndm ${⊢}{F}Fn{A}\to \mathrm{dom}{F}={A}$
4 3 eleq2d ${⊢}{F}Fn{A}\to \left({B}\in \mathrm{dom}{F}↔{B}\in {A}\right)$
5 2 4 syl5ib ${⊢}{F}Fn{A}\to \left({B}\in {{F}}^{-1}\left[{C}\right]\to {B}\in {A}\right)$
6 fnfun ${⊢}{F}Fn{A}\to \mathrm{Fun}{F}$
7 fvimacnvi ${⊢}\left(\mathrm{Fun}{F}\wedge {B}\in {{F}}^{-1}\left[{C}\right]\right)\to {F}\left({B}\right)\in {C}$
8 6 7 sylan ${⊢}\left({F}Fn{A}\wedge {B}\in {{F}}^{-1}\left[{C}\right]\right)\to {F}\left({B}\right)\in {C}$
9 8 ex ${⊢}{F}Fn{A}\to \left({B}\in {{F}}^{-1}\left[{C}\right]\to {F}\left({B}\right)\in {C}\right)$
10 5 9 jcad ${⊢}{F}Fn{A}\to \left({B}\in {{F}}^{-1}\left[{C}\right]\to \left({B}\in {A}\wedge {F}\left({B}\right)\in {C}\right)\right)$
11 fvimacnv ${⊢}\left(\mathrm{Fun}{F}\wedge {B}\in \mathrm{dom}{F}\right)\to \left({F}\left({B}\right)\in {C}↔{B}\in {{F}}^{-1}\left[{C}\right]\right)$
12 11 funfni ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({F}\left({B}\right)\in {C}↔{B}\in {{F}}^{-1}\left[{C}\right]\right)$
13 12 biimpd ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({F}\left({B}\right)\in {C}\to {B}\in {{F}}^{-1}\left[{C}\right]\right)$
14 13 expimpd ${⊢}{F}Fn{A}\to \left(\left({B}\in {A}\wedge {F}\left({B}\right)\in {C}\right)\to {B}\in {{F}}^{-1}\left[{C}\right]\right)$
15 10 14 impbid ${⊢}{F}Fn{A}\to \left({B}\in {{F}}^{-1}\left[{C}\right]↔\left({B}\in {A}\wedge {F}\left({B}\right)\in {C}\right)\right)$