Theorem fconst2

Description: A constant function expressed as a Cartesian product. (Contributed by NM, 20-Aug-1999)

	Ref	Expression
Hypothesis	fvconst2.1	$$⊢B\in \mathrm{V}$$
Assertion	fconst2	$$⊢F:A⟶\left\{B\right\}\leftrightarrow F=A\times \left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fvconst2.1	$$⊢B\in \mathrm{V}$$
2		fconst2g	$$⊢B\in \mathrm{V}\to \left(F:A⟶\left\{B\right\}\leftrightarrow F=A\times \left\{B\right\}\right)$$
3	1 2	ax-mp	$$⊢F:A⟶\left\{B\right\}\leftrightarrow F=A\times \left\{B\right\}$$