# Metamath Proof Explorer

## Theorem fvimacnv

Description: The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion fvimacnv
`|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )`

### Proof

Step Hyp Ref Expression
1 funfvop
` |-  ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )`
2 fvex
` |-  ( F ` A ) e. _V`
3 opelcnvg
` |-  ( ( ( F ` A ) e. _V /\ A e. dom F ) -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )`
4 2 3 mpan
` |-  ( A e. dom F -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )`
` |-  ( ( Fun F /\ A e. dom F ) -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )`
6 1 5 mpbird
` |-  ( ( Fun F /\ A e. dom F ) -> <. ( F ` A ) , A >. e. `' F )`
7 elimasng
` |-  ( ( ( F ` A ) e. _V /\ A e. dom F ) -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )`
8 2 7 mpan
` |-  ( A e. dom F -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )`
` |-  ( ( Fun F /\ A e. dom F ) -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )`
10 6 9 mpbird
` |-  ( ( Fun F /\ A e. dom F ) -> A e. ( `' F " { ( F ` A ) } ) )`
11 2 snss
` |-  ( ( F ` A ) e. B <-> { ( F ` A ) } C_ B )`
12 imass2
` |-  ( { ( F ` A ) } C_ B -> ( `' F " { ( F ` A ) } ) C_ ( `' F " B ) )`
13 11 12 sylbi
` |-  ( ( F ` A ) e. B -> ( `' F " { ( F ` A ) } ) C_ ( `' F " B ) )`
14 13 sseld
` |-  ( ( F ` A ) e. B -> ( A e. ( `' F " { ( F ` A ) } ) -> A e. ( `' F " B ) ) )`
15 10 14 syl5com
` |-  ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B -> A e. ( `' F " B ) ) )`
16 fvimacnvi
` |-  ( ( Fun F /\ A e. ( `' F " B ) ) -> ( F ` A ) e. B )`
17 16 ex
` |-  ( Fun F -> ( A e. ( `' F " B ) -> ( F ` A ) e. B ) )`
` |-  ( ( Fun F /\ A e. dom F ) -> ( A e. ( `' F " B ) -> ( F ` A ) e. B ) )`
` |-  ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )`