Theorem fnconstg

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

	Ref	Expression
Assertion	fnconstg	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fconstg	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } )
2	1	ffnd	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )