Metamath Proof Explorer

Theorem funimass4

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006)

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

Proof

Step Hyp Ref Expression
1 df-ss 
 |-  ( ( F " A ) C_ B <-> A. y ( y e. ( F " A ) -> y e. B ) )
2 vex 
 |-  y e. _V
3 2 elima 
 |-  ( y e. ( F " A ) <-> E. x e. A x F y )
4 eqcom 
 |-  ( y = ( F ` x ) <-> ( F ` x ) = y )
5 ssel 
 |-  ( A C_ dom F -> ( x e. A -> x e. dom F ) )
6 funbrfvb 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( F ` x ) = y <-> x F y ) )
7 6 ex 
 |-  ( Fun F -> ( x e. dom F -> ( ( F ` x ) = y <-> x F y ) ) )
8 5 7 syl9 
 |-  ( A C_ dom F -> ( Fun F -> ( x e. A -> ( ( F ` x ) = y <-> x F y ) ) ) )
9 8 imp31 
 |-  ( ( ( A C_ dom F /\ Fun F ) /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) )
10 4 9 bitrid 
 |-  ( ( ( A C_ dom F /\ Fun F ) /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) )
11 10 rexbidva 
 |-  ( ( A C_ dom F /\ Fun F ) -> ( E. x e. A y = ( F ` x ) <-> E. x e. A x F y ) )
12 3 11 bitr4id 
 |-  ( ( A C_ dom F /\ Fun F ) -> ( y e. ( F " A ) <-> E. x e. A y = ( F ` x ) ) )
13 12 imbi1d 
 |-  ( ( A C_ dom F /\ Fun F ) -> ( ( y e. ( F " A ) -> y e. B ) <-> ( E. x e. A y = ( F ` x ) -> y e. B ) ) )
14 r19.23v 
 |-  ( A. x e. A ( y = ( F ` x ) -> y e. B ) <-> ( E. x e. A y = ( F ` x ) -> y e. B ) )
15 13 14 bitr4di 
 |-  ( ( A C_ dom F /\ Fun F ) -> ( ( y e. ( F " A ) -> y e. B ) <-> A. x e. A ( y = ( F ` x ) -> y e. B ) ) )
16 15 albidv 
 |-  ( ( A C_ dom F /\ Fun F ) -> ( A. y ( y e. ( F " A ) -> y e. B ) <-> A. y A. x e. A ( y = ( F ` x ) -> y e. B ) ) )
17 ralcom4 
 |-  ( A. x e. A A. y ( y = ( F ` x ) -> y e. B ) <-> A. y A. x e. A ( y = ( F ` x ) -> y e. B ) )
18 fvex 
 |-  ( F ` x ) e. _V
19 eleq1 
 |-  ( y = ( F ` x ) -> ( y e. B <-> ( F ` x ) e. B ) )
20 18 19 ceqsalv 
 |-  ( A. y ( y = ( F ` x ) -> y e. B ) <-> ( F ` x ) e. B )
21 20 ralbii 
 |-  ( A. x e. A A. y ( y = ( F ` x ) -> y e. B ) <-> A. x e. A ( F ` x ) e. B )
22 17 21 bitr3i 
 |-  ( A. y A. x e. A ( y = ( F ` x ) -> y e. B ) <-> A. x e. A ( F ` x ) e. B )
23 16 22 bitrdi 
 |-  ( ( A C_ dom F /\ Fun F ) -> ( A. y ( y e. ( F " A ) -> y e. B ) <-> A. x e. A ( F ` x ) e. B ) )
24 1 23 bitrid 
 |-  ( ( A C_ dom F /\ Fun F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )
25 24 ancoms 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )