Theorem fvmpt2i

Description: Value of a function given by the maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypothesis	mptrcl.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	fvmpt2i	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( I ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		mptrcl.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		csbeq1	⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑥 / 𝑥 ⦌ 𝐵 )
3		csbid	⊢ ⦋ 𝑥 / 𝑥 ⦌ 𝐵 = 𝐵
4	2 3	eqtrdi	⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 )
5		nfcv	⊢ Ⅎ 𝑦 𝐵
6		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
7		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
8	5 6 7	cbvmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
9	1 8	eqtri	⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
10	4 9	fvmpti	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( I ‘ 𝐵 ) )