Theorem fconst6g

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

	Ref	Expression
Assertion	fconst6g	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fconstg	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } )
2		snssi	⊢ ( 𝐵 ∈ 𝐶 → { 𝐵 } ⊆ 𝐶 )
3	1 2	fssd	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ 𝐶 )