Metamath Proof Explorer

Theorem fvconst2

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

Ref Expression
Hypothesis fvconst2.1 
|- B e. _V
Assertion fvconst2 
|- ( C e. A -> ( ( A X. { B } ) ` C ) = B )

Proof

Step Hyp Ref Expression
1 fvconst2.1 
 |-  B e. _V
2 fvconst2g 
 |-  ( ( B e. _V /\ C e. A ) -> ( ( A X. { B } ) ` C ) = B )
3 1 2 mpan 
 |-  ( C e. A -> ( ( A X. { B } ) ` C ) = B )