Metamath Proof Explorer

Theorem fnconstg

Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014)

Ref Expression
Assertion fnconstg 
|- ( B e. V -> ( A X. { B } ) Fn A )

Proof

Step Hyp Ref Expression
1 fconstg 
 |-  ( B e. V -> ( A X. { B } ) : A --> { B } )
2 1 ffnd 
 |-  ( B e. V -> ( A X. { B } ) Fn A )