Theorem fvmpt

Description: Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011)

	Ref	Expression
Hypotheses	fvmptg.1	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
	fvmptg.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
	fvmpt.3	⊢ 𝐶 ∈ V
Assertion	fvmpt	⊢ ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fvmptg.1	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
2		fvmptg.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
3		fvmpt.3	⊢ 𝐶 ∈ V
4	1 2	fvmptg	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )
5	3 4	mpan2	⊢ ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )