Theorem fvmpts

Description: Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	fvmpts.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 ↦ 𝐵 )
Assertion	fvmpts	⊢ ( ( 𝐴 ∈ 𝐶 ∧ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fvmpts.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 ↦ 𝐵 )
2		csbeq1	⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
3		nfcv	⊢ Ⅎ 𝑦 𝐵
4		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
5		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
6	3 4 5	cbvmpt	⊢ ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐶 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
7	1 6	eqtri	⊢ 𝐹 = ( 𝑦 ∈ 𝐶 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
8	2 7	fvmptg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )