Description: Special case of fvmpt for operator theorems. (Contributed by NM, 27-Nov-2007)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fvmptmap.1 | |- C e. _V |
|
fvmptmap.2 | |- D e. _V |
||
fvmptmap.3 | |- R e. _V |
||
fvmptmap.4 | |- ( x = A -> B = C ) |
||
fvmptmap.5 | |- F = ( x e. ( R ^m D ) |-> B ) |
||
Assertion | fvmptmap | |- ( A : D --> R -> ( F ` A ) = C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvmptmap.1 | |- C e. _V |
|
2 | fvmptmap.2 | |- D e. _V |
|
3 | fvmptmap.3 | |- R e. _V |
|
4 | fvmptmap.4 | |- ( x = A -> B = C ) |
|
5 | fvmptmap.5 | |- F = ( x e. ( R ^m D ) |-> B ) |
|
6 | 3 2 | elmap | |- ( A e. ( R ^m D ) <-> A : D --> R ) |
7 | 4 5 1 | fvmpt | |- ( A e. ( R ^m D ) -> ( F ` A ) = C ) |
8 | 6 7 | sylbir | |- ( A : D --> R -> ( F ` A ) = C ) |