Theorem fconst6

Description: A constant function as a mapping. (Contributed by Jeff Madsen, 30-Nov-2009) (Revised by Mario Carneiro, 22-Apr-2015)

	Ref	Expression
Hypothesis	fconst6.1	⊢ 𝐵 ∈ 𝐶
Assertion	fconst6	⊢ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ 𝐶

Proof

Step	Hyp	Ref	Expression
1		fconst6.1	⊢ 𝐵 ∈ 𝐶
2		fconst6g	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ 𝐶 )
3	1 2	ax-mp	⊢ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ 𝐶