Theorem fconstg

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

	Ref	Expression
Assertion	fconstg	$$⊢B\in V\to \left(A\times \left\{B\right\}\right):A⟶\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		sneq	$$⊢x=B\to \left\{x\right\}=\left\{B\right\}$$
2	1	xpeq2d	$$⊢x=B\to A\times \left\{x\right\}=A\times \left\{B\right\}$$
3		feq1	$$⊢A\times \left\{x\right\}=A\times \left\{B\right\}\to \left(\left(A\times \left\{x\right\}\right):A⟶\left\{x\right\}\leftrightarrow \left(A\times \left\{B\right\}\right):A⟶\left\{x\right\}\right)$$
4		feq3	$$⊢\left\{x\right\}=\left\{B\right\}\to \left(\left(A\times \left\{B\right\}\right):A⟶\left\{x\right\}\leftrightarrow \left(A\times \left\{B\right\}\right):A⟶\left\{B\right\}\right)$$
5	3 4	sylan9bb	$$⊢\left(A\times \left\{x\right\}=A\times \left\{B\right\}\wedge \left\{x\right\}=\left\{B\right\}\right)\to \left(\left(A\times \left\{x\right\}\right):A⟶\left\{x\right\}\leftrightarrow \left(A\times \left\{B\right\}\right):A⟶\left\{B\right\}\right)$$
6	2 1 5	syl2anc	$$⊢x=B\to \left(\left(A\times \left\{x\right\}\right):A⟶\left\{x\right\}\leftrightarrow \left(A\times \left\{B\right\}\right):A⟶\left\{B\right\}\right)$$
7		vex	$$⊢x\in \mathrm{V}$$
8	7	fconst	$$⊢\left(A\times \left\{x\right\}\right):A⟶\left\{x\right\}$$
9	6 8	vtoclg	$$⊢B\in V\to \left(A\times \left\{B\right\}\right):A⟶\left\{B\right\}$$