Step |
Hyp |
Ref |
Expression |
1 |
|
dfss2 |
|- ( ( 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 ) ) |