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 )