Metamath Proof Explorer

Theorem fvelimab

Description: Function value in an image. (Contributed by NM, 20-Jan-2007) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Revised by David Abernethy, 17-Dec-2011)

Ref Expression
Assertion fvelimab 
|- ( ( F Fn A /\ B C_ A ) -> ( C e. ( F " B ) <-> E. x e. B ( F ` x ) = C ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( C e. ( F " B ) -> C e. _V )
2 1 anim2i 
 |-  ( ( ( F Fn A /\ B C_ A ) /\ C e. ( F " B ) ) -> ( ( F Fn A /\ B C_ A ) /\ C e. _V ) )
3 fvex 
 |-  ( F ` x ) e. _V
4 eleq1 
 |-  ( ( F ` x ) = C -> ( ( F ` x ) e. _V <-> C e. _V ) )
5 3 4 mpbii 
 |-  ( ( F ` x ) = C -> C e. _V )
6 5 rexlimivw 
 |-  ( E. x e. B ( F ` x ) = C -> C e. _V )
7 6 anim2i 
 |-  ( ( ( F Fn A /\ B C_ A ) /\ E. x e. B ( F ` x ) = C ) -> ( ( F Fn A /\ B C_ A ) /\ C e. _V ) )
8 eleq1 
 |-  ( y = C -> ( y e. ( F " B ) <-> C e. ( F " B ) ) )
9 eqeq2 
 |-  ( y = C -> ( ( F ` x ) = y <-> ( F ` x ) = C ) )
10 9 rexbidv 
 |-  ( y = C -> ( E. x e. B ( F ` x ) = y <-> E. x e. B ( F ` x ) = C ) )
11 8 10 bibi12d 
 |-  ( y = C -> ( ( y e. ( F " B ) <-> E. x e. B ( F ` x ) = y ) <-> ( C e. ( F " B ) <-> E. x e. B ( F ` x ) = C ) ) )
12 11 imbi2d 
 |-  ( y = C -> ( ( ( F Fn A /\ B C_ A ) -> ( y e. ( F " B ) <-> E. x e. B ( F ` x ) = y ) ) <-> ( ( F Fn A /\ B C_ A ) -> ( C e. ( F " B ) <-> E. x e. B ( F ` x ) = C ) ) ) )
13 fnfun 
 |-  ( F Fn A -> Fun F )
14 fndm 
 |-  ( F Fn A -> dom F = A )
15 14 sseq2d 
 |-  ( F Fn A -> ( B C_ dom F <-> B C_ A ) )
16 15 biimpar 
 |-  ( ( F Fn A /\ B C_ A ) -> B C_ dom F )
17 dfimafn 
 |-  ( ( Fun F /\ B C_ dom F ) -> ( F " B ) = { y | E. x e. B ( F ` x ) = y } )
18 13 16 17 syl2an2r 
 |-  ( ( F Fn A /\ B C_ A ) -> ( F " B ) = { y | E. x e. B ( F ` x ) = y } )
19 18 abeq2d 
 |-  ( ( F Fn A /\ B C_ A ) -> ( y e. ( F " B ) <-> E. x e. B ( F ` x ) = y ) )
20 12 19 vtoclg 
 |-  ( C e. _V -> ( ( F Fn A /\ B C_ A ) -> ( C e. ( F " B ) <-> E. x e. B ( F ` x ) = C ) ) )
21 20 impcom 
 |-  ( ( ( F Fn A /\ B C_ A ) /\ C e. _V ) -> ( C e. ( F " B ) <-> E. x e. B ( F ` x ) = C ) )
22 2 7 21 pm5.21nd 
 |-  ( ( F Fn A /\ B C_ A ) -> ( C e. ( F " B ) <-> E. x e. B ( F ` x ) = C ) )