Theorem fvmpt2

Description: Value of a function given by the maps-to notation. (Contributed by FL, 21-Jun-2010)

	Ref	Expression
Hypothesis	mptrcl.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mptrcl.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2	1	fvmpt2i	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( I ‘ 𝐵 ) )
3		fvi	⊢ ( 𝐵 ∈ 𝐶 → ( I ‘ 𝐵 ) = 𝐵 )
4	2 3	sylan9eq	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )