Theorem fvmpt2df

Description: Deduction version of fvmpt2 . (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	fvmpt2df.1	⊢ Ⅎ 𝑥 𝐴
	fvmpt2df.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	fvmpt2df.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion	fvmpt2df	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fvmpt2df.1	⊢ Ⅎ 𝑥 𝐴
2		fvmpt2df.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3		fvmpt2df.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4	2	fveq1i	⊢ ( 𝐹 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
5		id	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴 )
6	1	fvmpt2f	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
7	5 3 6	syl2an2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
8	4 7	eqtrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )