Theorem fvmptg

Description: Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007) (Revised by Mario Carneiro, 31-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		fvmptg.1	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
2		fvmptg.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
3		eqid	⊢ 𝐶 = 𝐶
4	1	eqeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝑦 = 𝐵 ↔ 𝑦 = 𝐶 ) )
5		eqeq1	⊢ ( 𝑦 = 𝐶 → ( 𝑦 = 𝐶 ↔ 𝐶 = 𝐶 ) )
6		moeq	⊢ ∃* 𝑦 𝑦 = 𝐵
7	6	a1i	⊢ ( 𝑥 ∈ 𝐷 → ∃* 𝑦 𝑦 = 𝐵 )
8		df-mpt	⊢ ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵 ) }
9	2 8	eqtri	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵 ) }
10	4 5 7 9	fvopab3ig	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ) → ( 𝐶 = 𝐶 → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) )
11	3 10	mpi	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )