Theorem fvmpt2d

Description: Deduction version of fvmpt2 . (Contributed by Thierry Arnoux, 8-Dec-2016)

	Ref	Expression
Hypotheses	fvmpt2d.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
	fvmpt2d.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fvmpt2d.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
2		fvmpt2d.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3	1	fveq1d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
4	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
5		id	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴 )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	6	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
8	5 2 7	syl2an2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
9	4 8	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )