Theorem fvconst

Description: The value of a constant function. (Contributed by NM, 30-May-1999)

	Ref	Expression
Assertion	fvconst	$$⊢\left(F:A⟶\left\{B\right\}\wedge C\in A\right)\to F\left(C\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		ffvelrn	$$⊢\left(F:A⟶\left\{B\right\}\wedge C\in A\right)\to F\left(C\right)\in \left\{B\right\}$$
2		elsni	$$⊢F\left(C\right)\in \left\{B\right\}\to F\left(C\right)=B$$
3	1 2	syl	$$⊢\left(F:A⟶\left\{B\right\}\wedge C\in A\right)\to F\left(C\right)=B$$