Step |
Hyp |
Ref |
Expression |
1 |
|
imassmpt.1 |
|- F/ x ph |
2 |
|
imassmpt.2 |
|- ( ( ph /\ x e. ( A i^i C ) ) -> B e. V ) |
3 |
|
imassmpt.3 |
|- F = ( x e. A |-> B ) |
4 |
|
df-ima |
|- ( F " C ) = ran ( F |` C ) |
5 |
3
|
reseq1i |
|- ( F |` C ) = ( ( x e. A |-> B ) |` C ) |
6 |
|
resmpt3 |
|- ( ( x e. A |-> B ) |` C ) = ( x e. ( A i^i C ) |-> B ) |
7 |
5 6
|
eqtri |
|- ( F |` C ) = ( x e. ( A i^i C ) |-> B ) |
8 |
7
|
rneqi |
|- ran ( F |` C ) = ran ( x e. ( A i^i C ) |-> B ) |
9 |
4 8
|
eqtri |
|- ( F " C ) = ran ( x e. ( A i^i C ) |-> B ) |
10 |
9
|
sseq1i |
|- ( ( F " C ) C_ D <-> ran ( x e. ( A i^i C ) |-> B ) C_ D ) |
11 |
|
eqid |
|- ( x e. ( A i^i C ) |-> B ) = ( x e. ( A i^i C ) |-> B ) |
12 |
1 11 2
|
rnmptssbi |
|- ( ph -> ( ran ( x e. ( A i^i C ) |-> B ) C_ D <-> A. x e. ( A i^i C ) B e. D ) ) |
13 |
10 12
|
syl5bb |
|- ( ph -> ( ( F " C ) C_ D <-> A. x e. ( A i^i C ) B e. D ) ) |