Step |
Hyp |
Ref |
Expression |
1 |
|
ralima.x |
|- ( x = ( F ` y ) -> ( ph <-> ps ) ) |
2 |
|
fnfun |
|- ( F Fn A -> Fun F ) |
3 |
2
|
funfnd |
|- ( F Fn A -> F Fn dom F ) |
4 |
|
fndm |
|- ( F Fn A -> dom F = A ) |
5 |
4
|
sseq2d |
|- ( F Fn A -> ( B C_ dom F <-> B C_ A ) ) |
6 |
5
|
biimpar |
|- ( ( F Fn A /\ B C_ A ) -> B C_ dom F ) |
7 |
|
fvexd |
|- ( ( ( F Fn dom F /\ B C_ dom F ) /\ y e. B ) -> ( F ` y ) e. _V ) |
8 |
|
fvelimab |
|- ( ( F Fn dom F /\ B C_ dom F ) -> ( x e. ( F " B ) <-> E. y e. B ( F ` y ) = x ) ) |
9 |
|
eqcom |
|- ( ( F ` y ) = x <-> x = ( F ` y ) ) |
10 |
9
|
rexbii |
|- ( E. y e. B ( F ` y ) = x <-> E. y e. B x = ( F ` y ) ) |
11 |
8 10
|
bitrdi |
|- ( ( F Fn dom F /\ B C_ dom F ) -> ( x e. ( F " B ) <-> E. y e. B x = ( F ` y ) ) ) |
12 |
1
|
adantl |
|- ( ( ( F Fn dom F /\ B C_ dom F ) /\ x = ( F ` y ) ) -> ( ph <-> ps ) ) |
13 |
7 11 12
|
ralxfr2d |
|- ( ( F Fn dom F /\ B C_ dom F ) -> ( A. x e. ( F " B ) ph <-> A. y e. B ps ) ) |
14 |
3 6 13
|
syl2an2r |
|- ( ( F Fn A /\ B C_ A ) -> ( A. x e. ( F " B ) ph <-> A. y e. B ps ) ) |