Theorem fvmptmap

Description: Special case of fvmpt for operator theorems. (Contributed by NM, 27-Nov-2007)

	Ref	Expression
Hypotheses	fvmptmap.1	⊢ 𝐶 ∈ V
	fvmptmap.2	⊢ 𝐷 ∈ V
	fvmptmap.3	⊢ 𝑅 ∈ V
	fvmptmap.4	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
	fvmptmap.5	⊢ 𝐹 = ( 𝑥 ∈ ( 𝑅 ↑m 𝐷 ) ↦ 𝐵 )
Assertion	fvmptmap	⊢ ( 𝐴 : 𝐷 ⟶ 𝑅 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fvmptmap.1	⊢ 𝐶 ∈ V
2		fvmptmap.2	⊢ 𝐷 ∈ V
3		fvmptmap.3	⊢ 𝑅 ∈ V
4		fvmptmap.4	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
5		fvmptmap.5	⊢ 𝐹 = ( 𝑥 ∈ ( 𝑅 ↑m 𝐷 ) ↦ 𝐵 )
6	3 2	elmap	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝐷 ) ↔ 𝐴 : 𝐷 ⟶ 𝑅 )
7	4 5 1	fvmpt	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝐷 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )
8	6 7	sylbir	⊢ ( 𝐴 : 𝐷 ⟶ 𝑅 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )