Metamath Proof Explorer

Theorem fvconst

Description: The value of a constant function. (Contributed by NM, 30-May-1999)

Ref Expression
Assertion fvconst 
|- ( ( F : A --> { B } /\ C e. A ) -> ( F ` C ) = B )

Proof

Step Hyp Ref Expression
1 ffvelrn 
 |-  ( ( F : A --> { B } /\ C e. A ) -> ( F ` C ) e. { B } )
2 elsni 
 |-  ( ( F ` C ) e. { B } -> ( F ` C ) = B )
3 1 2 syl 
 |-  ( ( F : A --> { B } /\ C e. A ) -> ( F ` C ) = B )