Theorem fconst

Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 14-Aug-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Hypothesis	fconst.1	|- B e. _V
Assertion	fconst	|- ( A X. { B } ) : A --> { B }

Proof

Step	Hyp	Ref	Expression
1		fconst.1	|- B e. _V
2		fconstmpt	|- ( A X. { B } ) = ( x e. A |-> B )
3	1 2	fnmpti	|- ( A X. { B } ) Fn A
4		rnxpss	|- ran ( A X. { B } ) C_ { B }
5		df-f	|- ( ( A X. { B } ) : A --> { B } <-> ( ( A X. { B } ) Fn A /\ ran ( A X. { B } ) C_ { B } ) )
6	3 4 5	mpbir2an	|- ( A X. { B } ) : A --> { B }