Theorem fvmpt2

Description: Value of a function given by the maps-to notation. (Contributed by FL, 21-Jun-2010)

	Ref	Expression
Hypothesis	mptrcl.1	|- F = ( x e. A |-> B )
Assertion	fvmpt2	|- ( ( x e. A /\ B e. C ) -> ( F ` x ) = B )

Proof

Step	Hyp	Ref	Expression
1		mptrcl.1	|- F = ( x e. A |-> B )
2	1	fvmpt2i	|- ( x e. A -> ( F ` x ) = ( _I ` B ) )
3		fvi	|- ( B e. C -> ( _I ` B ) = B )
4	2 3	sylan9eq	|- ( ( x e. A /\ B e. C ) -> ( F ` x ) = B )