Theorem fvconst2

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

	Ref	Expression
Hypothesis	fvconst2.1	⊢ 𝐵 ∈ V
Assertion	fvconst2	⊢ ( 𝐶 ∈ 𝐴 → ( ( 𝐴 × { 𝐵 } ) ‘ 𝐶 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fvconst2.1	⊢ 𝐵 ∈ V
2		fvconst2g	⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝐶 ) = 𝐵 )
3	1 2	mpan	⊢ ( 𝐶 ∈ 𝐴 → ( ( 𝐴 × { 𝐵 } ) ‘ 𝐶 ) = 𝐵 )