This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐶 ) ∈ { 𝐵 } )
2 elsni ⊢ ( ( 𝐹 ‘ 𝐶 ) ∈ { 𝐵 } → ( 𝐹 ‘ 𝐶 ) = 𝐵 )
3 1 2 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐶 ) = 𝐵 )