Step |
Hyp |
Ref |
Expression |
1 |
|
ssint |
|- ( C C_ |^| ( F " B ) <-> A. y e. ( F " B ) C C_ y ) |
2 |
|
df-ral |
|- ( A. y e. ( F " B ) C C_ y <-> A. y ( y e. ( F " B ) -> C C_ y ) ) |
3 |
1 2
|
bitri |
|- ( C C_ |^| ( F " B ) <-> A. y ( y e. ( F " B ) -> C C_ y ) ) |
4 |
|
fvelimab |
|- ( ( F Fn A /\ B C_ A ) -> ( y e. ( F " B ) <-> E. x e. B ( F ` x ) = y ) ) |
5 |
4
|
imbi1d |
|- ( ( F Fn A /\ B C_ A ) -> ( ( y e. ( F " B ) -> C C_ y ) <-> ( E. x e. B ( F ` x ) = y -> C C_ y ) ) ) |
6 |
5
|
albidv |
|- ( ( F Fn A /\ B C_ A ) -> ( A. y ( y e. ( F " B ) -> C C_ y ) <-> A. y ( E. x e. B ( F ` x ) = y -> C C_ y ) ) ) |
7 |
|
ralcom4 |
|- ( A. x e. B A. y ( ( F ` x ) = y -> C C_ y ) <-> A. y A. x e. B ( ( F ` x ) = y -> C C_ y ) ) |
8 |
|
eqcom |
|- ( ( F ` x ) = y <-> y = ( F ` x ) ) |
9 |
8
|
imbi1i |
|- ( ( ( F ` x ) = y -> C C_ y ) <-> ( y = ( F ` x ) -> C C_ y ) ) |
10 |
9
|
albii |
|- ( A. y ( ( F ` x ) = y -> C C_ y ) <-> A. y ( y = ( F ` x ) -> C C_ y ) ) |
11 |
|
fvex |
|- ( F ` x ) e. _V |
12 |
|
sseq2 |
|- ( y = ( F ` x ) -> ( C C_ y <-> C C_ ( F ` x ) ) ) |
13 |
11 12
|
ceqsalv |
|- ( A. y ( y = ( F ` x ) -> C C_ y ) <-> C C_ ( F ` x ) ) |
14 |
10 13
|
bitri |
|- ( A. y ( ( F ` x ) = y -> C C_ y ) <-> C C_ ( F ` x ) ) |
15 |
14
|
ralbii |
|- ( A. x e. B A. y ( ( F ` x ) = y -> C C_ y ) <-> A. x e. B C C_ ( F ` x ) ) |
16 |
|
r19.23v |
|- ( A. x e. B ( ( F ` x ) = y -> C C_ y ) <-> ( E. x e. B ( F ` x ) = y -> C C_ y ) ) |
17 |
16
|
albii |
|- ( A. y A. x e. B ( ( F ` x ) = y -> C C_ y ) <-> A. y ( E. x e. B ( F ` x ) = y -> C C_ y ) ) |
18 |
7 15 17
|
3bitr3ri |
|- ( A. y ( E. x e. B ( F ` x ) = y -> C C_ y ) <-> A. x e. B C C_ ( F ` x ) ) |
19 |
6 18
|
bitrdi |
|- ( ( F Fn A /\ B C_ A ) -> ( A. y ( y e. ( F " B ) -> C C_ y ) <-> A. x e. B C C_ ( F ` x ) ) ) |
20 |
3 19
|
syl5bb |
|- ( ( F Fn A /\ B C_ A ) -> ( C C_ |^| ( F " B ) <-> A. x e. B C C_ ( F ` x ) ) ) |