Theorem fvmpt3i

Description: Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	fvmpt3.a	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
	fvmpt3.b	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
	fvmpt3i.c	⊢ 𝐵 ∈ V
Assertion	fvmpt3i	⊢ ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fvmpt3.a	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
2		fvmpt3.b	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
3		fvmpt3i.c	⊢ 𝐵 ∈ V
4	3	a1i	⊢ ( 𝑥 ∈ 𝐷 → 𝐵 ∈ V )
5	1 2 4	fvmpt3	⊢ ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )