Metamath Proof Explorer

Theorem fconst2

Description: A constant function expressed as a Cartesian product. (Contributed by NM, 20-Aug-1999)

Ref Expression
Hypothesis fvconst2.1 
|- B e. _V
Assertion fconst2 
|- ( F : A --> { B } <-> F = ( A X. { B } ) )

Proof

Step Hyp Ref Expression
1 fvconst2.1 
 |-  B e. _V
2 fconst2g 
 |-  ( B e. _V -> ( F : A --> { B } <-> F = ( A X. { B } ) ) )
3 1 2 ax-mp 
 |-  ( F : A --> { B } <-> F = ( A X. { B } ) )