Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | fnconstg | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconstg | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } ) | |
2 | 1 | ffnd | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 ) |