# Metamath Proof Explorer

## Theorem fconstg

Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 19-Oct-2004)

Ref Expression
Assertion fconstg ${⊢}{B}\in {V}\to \left({A}×\left\{{B}\right\}\right):{A}⟶\left\{{B}\right\}$

### Proof

Step Hyp Ref Expression
1 sneq ${⊢}{x}={B}\to \left\{{x}\right\}=\left\{{B}\right\}$
2 1 xpeq2d ${⊢}{x}={B}\to {A}×\left\{{x}\right\}={A}×\left\{{B}\right\}$
3 feq1 ${⊢}{A}×\left\{{x}\right\}={A}×\left\{{B}\right\}\to \left(\left({A}×\left\{{x}\right\}\right):{A}⟶\left\{{x}\right\}↔\left({A}×\left\{{B}\right\}\right):{A}⟶\left\{{x}\right\}\right)$
4 feq3 ${⊢}\left\{{x}\right\}=\left\{{B}\right\}\to \left(\left({A}×\left\{{B}\right\}\right):{A}⟶\left\{{x}\right\}↔\left({A}×\left\{{B}\right\}\right):{A}⟶\left\{{B}\right\}\right)$
5 3 4 sylan9bb ${⊢}\left({A}×\left\{{x}\right\}={A}×\left\{{B}\right\}\wedge \left\{{x}\right\}=\left\{{B}\right\}\right)\to \left(\left({A}×\left\{{x}\right\}\right):{A}⟶\left\{{x}\right\}↔\left({A}×\left\{{B}\right\}\right):{A}⟶\left\{{B}\right\}\right)$
6 2 1 5 syl2anc ${⊢}{x}={B}\to \left(\left({A}×\left\{{x}\right\}\right):{A}⟶\left\{{x}\right\}↔\left({A}×\left\{{B}\right\}\right):{A}⟶\left\{{B}\right\}\right)$
7 vex ${⊢}{x}\in \mathrm{V}$
8 7 fconst ${⊢}\left({A}×\left\{{x}\right\}\right):{A}⟶\left\{{x}\right\}$
9 6 8 vtoclg ${⊢}{B}\in {V}\to \left({A}×\left\{{B}\right\}\right):{A}⟶\left\{{B}\right\}$