Theorem fvmpti

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

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

Proof

Step	Hyp	Ref	Expression
1		fvmptg.1	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
2		fvmptg.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
3	1 2	fvmptg	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )
4		fvi	⊢ ( 𝐶 ∈ V → ( I ‘ 𝐶 ) = 𝐶 )
5	4	adantl	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V ) → ( I ‘ 𝐶 ) = 𝐶 )
6	3 5	eqtr4d	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = ( I ‘ 𝐶 ) )
7	1	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∈ V ↔ 𝐶 ∈ V ) )
8	2	dmmpt	⊢ dom 𝐹 = { 𝑥 ∈ 𝐷 ∣ 𝐵 ∈ V }
9	7 8	elrab2	⊢ ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V ) )
10	9	baib	⊢ ( 𝐴 ∈ 𝐷 → ( 𝐴 ∈ dom 𝐹 ↔ 𝐶 ∈ V ) )
11	10	notbid	⊢ ( 𝐴 ∈ 𝐷 → ( ¬ 𝐴 ∈ dom 𝐹 ↔ ¬ 𝐶 ∈ V ) )
12		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
13	11 12	syl6bir	⊢ ( 𝐴 ∈ 𝐷 → ( ¬ 𝐶 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ ) )
14	13	imp	⊢ ( ( 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
15		fvprc	⊢ ( ¬ 𝐶 ∈ V → ( I ‘ 𝐶 ) = ∅ )
16	15	adantl	⊢ ( ( 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ V ) → ( I ‘ 𝐶 ) = ∅ )
17	14 16	eqtr4d	⊢ ( ( 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = ( I ‘ 𝐶 ) )
18	6 17	pm2.61dan	⊢ ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = ( I ‘ 𝐶 ) )