Metamath Proof Explorer

Theorem fvconst2g

Description: The value of a constant function. (Contributed by NM, 20-Aug-2005)

Ref Expression
Assertion fvconst2g 
|- ( ( B e. D /\ C e. A ) -> ( ( A X. { B } ) ` C ) = B )

Proof

Step Hyp Ref Expression
1 fconstg 
 |-  ( B e. D -> ( A X. { B } ) : A --> { B } )
2 fvconst 
 |-  ( ( ( A X. { B } ) : A --> { B } /\ C e. A ) -> ( ( A X. { B } ) ` C ) = B )
3 1 2 sylan 
 |-  ( ( B e. D /\ C e. A ) -> ( ( A X. { B } ) ` C ) = B )