Theorem fconst6g

Description: Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		fconstg	$$⊢B\in C\to \left(A\times \left\{B\right\}\right):A⟶\left\{B\right\}$$
2		snssi	$$⊢B\in C\to \left\{B\right\}\subseteq C$$
3	1 2	fssd	$$⊢B\in C\to \left(A\times \left\{B\right\}\right):A⟶C$$