This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fconstg

Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 19-Oct-2004)

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

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( x = B -> { x } = { B } )
2 1 xpeq2d 
 |-  ( x = B -> ( A X. { x } ) = ( A X. { B } ) )
3 feq1 
 |-  ( ( A X. { x } ) = ( A X. { B } ) -> ( ( A X. { x } ) : A --> { x } <-> ( A X. { B } ) : A --> { x } ) )
4 feq3 
 |-  ( { x } = { B } -> ( ( A X. { B } ) : A --> { x } <-> ( A X. { B } ) : A --> { B } ) )
5 3 4 sylan9bb 
 |-  ( ( ( A X. { x } ) = ( A X. { B } ) /\ { x } = { B } ) -> ( ( A X. { x } ) : A --> { x } <-> ( A X. { B } ) : A --> { B } ) )
6 2 1 5 syl2anc 
 |-  ( x = B -> ( ( A X. { x } ) : A --> { x } <-> ( A X. { B } ) : A --> { B } ) )
7 vex 
 |-  x e. _V
8 7 fconst 
 |-  ( A X. { x } ) : A --> { x }
9 6 8 vtoclg 
 |-  ( B e. V -> ( A X. { B } ) : A --> { B } )