Metamath Proof Explorer


Theorem fvmptmap

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 )

Proof

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 )