Theorem fvconst

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

	Ref	Expression
Assertion	fvconst	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐶 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ffvelrn	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐶 ) ∈ { 𝐵 } )
2		elsni	⊢ ( ( 𝐹 ‘ 𝐶 ) ∈ { 𝐵 } → ( 𝐹 ‘ 𝐶 ) = 𝐵 )
3	1 2	syl	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐶 ) = 𝐵 )