Theorem fvmpt2bd

Description: Value of a function given by the maps-to notation. Deduction version. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypothesis	fvmpt2bd.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
Assertion	fvmpt2bd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fvmpt2bd.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
2	1	fveq1d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
3	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	4	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
6	5	3adant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
7	3 6	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )