Step |
Hyp |
Ref |
Expression |
1 |
|
ofcfval2.1 |
|- ( ph -> A e. V ) |
2 |
|
ofcfval2.2 |
|- ( ph -> C e. W ) |
3 |
|
ofcfval2.3 |
|- ( ( ph /\ x e. A ) -> B e. X ) |
4 |
|
ofcfval2.4 |
|- ( ph -> F = ( x e. A |-> B ) ) |
5 |
3
|
ralrimiva |
|- ( ph -> A. x e. A B e. X ) |
6 |
|
eqid |
|- ( x e. A |-> B ) = ( x e. A |-> B ) |
7 |
6
|
fnmpt |
|- ( A. x e. A B e. X -> ( x e. A |-> B ) Fn A ) |
8 |
5 7
|
syl |
|- ( ph -> ( x e. A |-> B ) Fn A ) |
9 |
4
|
fneq1d |
|- ( ph -> ( F Fn A <-> ( x e. A |-> B ) Fn A ) ) |
10 |
8 9
|
mpbird |
|- ( ph -> F Fn A ) |
11 |
4 3
|
fvmpt2d |
|- ( ( ph /\ x e. A ) -> ( F ` x ) = B ) |
12 |
10 1 2 11
|
ofcfval |
|- ( ph -> ( F oFC R C ) = ( x e. A |-> ( B R C ) ) ) |