Theorem fvmptd3

Description: Deduction version of fvmpt . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	fvmptd3.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
	fvmptd3.2	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
	fvmptd3.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	fvmptd3.4	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
Assertion	fvmptd3	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fvmptd3.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
2		fvmptd3.2	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
3		fvmptd3.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
4		fvmptd3.4	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5	2 1	fvmptg	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )
6	3 4 5	syl2anc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )