Metamath Proof Explorer


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 )