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 } )