Description: Value of a function given in mapsto notation. (Contributed by NM, 17Aug2011)
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 ) 
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 ) 