Theorem fvmpt2f

Description: Value of a function given by the maps-to notation. (Contributed by Thierry Arnoux, 9-Mar-2017)

	Ref	Expression
Hypothesis	fvmpt2f.0	⊢ Ⅎ 𝑥 𝐴
Assertion	fvmpt2f	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fvmpt2f.0	⊢ Ⅎ 𝑥 𝐴
2		csbeq1	⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑥 / 𝑥 ⦌ 𝐵 )
3		csbid	⊢ ⦋ 𝑥 / 𝑥 ⦌ 𝐵 = 𝐵
4	2 3	eqtrdi	⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 )
5		nfcv	⊢ Ⅎ 𝑦 𝐴
6		nfcv	⊢ Ⅎ 𝑦 𝐵
7		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
8		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
9	1 5 6 7 8	cbvmptf	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
10	4 9	fvmptg	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )