Theorem fvconst2

Description: The value of a constant function. (Contributed by NM, 16-Apr-2005)

	Ref	Expression
Hypothesis	fvconst2.1	$$⊢B\in \mathrm{V}$$
Assertion	fvconst2	$$⊢C\in A\to \left(A\times \left\{B\right\}\right)\left(C\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		fvconst2.1	$$⊢B\in \mathrm{V}$$
2		fvconst2g	$$⊢\left(B\in \mathrm{V}\wedge C\in A\right)\to \left(A\times \left\{B\right\}\right)\left(C\right)=B$$
3	1 2	mpan	$$⊢C\in A\to \left(A\times \left\{B\right\}\right)\left(C\right)=B$$