Metamath Proof Explorer


Theorem fvconst

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

Ref Expression
Assertion fvconst F:ABCAFC=B

Proof

Step Hyp Ref Expression
1 ffvelcdm F:ABCAFCB
2 elsni FCBFC=B
3 1 2 syl F:ABCAFC=B