Theorem fvmpt

Description: Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011)

	Ref	Expression
Hypotheses	fvmptg.1	|- ( x = A -> B = C )
	fvmptg.2	|- F = ( x e. D |-> B )
	fvmpt.3	|- C e. _V
Assertion	fvmpt	|- ( A e. D -> ( F ` A ) = C )

Proof

Step	Hyp	Ref	Expression
1		fvmptg.1	|- ( x = A -> B = C )
2		fvmptg.2	|- F = ( x e. D |-> B )
3		fvmpt.3	|- C e. _V
4	1 2	fvmptg	|- ( ( A e. D /\ C e. _V ) -> ( F ` A ) = C )
5	3 4	mpan2	|- ( A e. D -> ( F ` A ) = C )