Theorem fnconstg

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

	Ref	Expression
Assertion	fnconstg	$$⊢B\in V\to \left(A\times \left\{B\right\}\right)FnA$$

Proof

Step	Hyp	Ref	Expression
1		fconstg	$$⊢B\in V\to \left(A\times \left\{B\right\}\right):A⟶\left\{B\right\}$$
2	1	ffnd	$$⊢B\in V\to \left(A\times \left\{B\right\}\right)FnA$$