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 
|- ( ( Fun F /\ A e. ( `' F " B ) ) -> ( F ` A ) e. B )

Proof

Step Hyp Ref Expression
1 snssi 
 |-  ( A e. ( `' F " B ) -> { A } C_ ( `' F " B ) )
2 funimass2 
 |-  ( ( Fun F /\ { A } C_ ( `' F " B ) ) -> ( F " { A } ) C_ B )
3 1 2 sylan2 
 |-  ( ( Fun F /\ A e. ( `' F " B ) ) -> ( F " { A } ) C_ B )
4 fvex 
 |-  ( F ` A ) e. _V
5 4 snss 
 |-  ( ( F ` A ) e. B <-> { ( F ` A ) } C_ B )
6 cnvimass 
 |-  ( `' F " B ) C_ dom F
7 6 sseli 
 |-  ( A e. ( `' F " B ) -> A e. dom F )
8 funfn 
 |-  ( Fun F <-> F Fn dom F )
9 fnsnfv 
 |-  ( ( F Fn dom F /\ A e. dom F ) -> { ( F ` A ) } = ( F " { A } ) )
10 8 9 sylanb 
 |-  ( ( Fun F /\ A e. dom F ) -> { ( F ` A ) } = ( F " { A } ) )
11 7 10 sylan2 
 |-  ( ( Fun F /\ A e. ( `' F " B ) ) -> { ( F ` A ) } = ( F " { A } ) )
12 11 sseq1d 
 |-  ( ( Fun F /\ A e. ( `' F " B ) ) -> ( { ( F ` A ) } C_ B <-> ( F " { A } ) C_ B ) )
13 5 12 bitrid 
 |-  ( ( Fun F /\ A e. ( `' F " B ) ) -> ( ( F ` A ) e. B <-> ( F " { A } ) C_ B ) )
14 3 13 mpbird 
 |-  ( ( Fun F /\ A e. ( `' F " B ) ) -> ( F ` A ) e. B )