Theorem fvconst2g

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

	Ref	Expression
Assertion	fvconst2g	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝐶 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fconstg	⊢ ( 𝐵 ∈ 𝐷 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } )
2		fvconst	⊢ ( ( ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } ∧ 𝐶 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝐶 ) = 𝐵 )
3	1 2	sylan	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝐶 ) = 𝐵 )