Theorem fvmpt4d

Description: Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 15-Feb-2025)

	Ref	Expression
Hypotheses	fvmpt4d.1	⊢ Ⅎ 𝑥 𝐴
	fvmpt4d.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
	fvmpt4d.3	⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
Assertion	fvmpt4d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fvmpt4d.1	⊢ Ⅎ 𝑥 𝐴
2		fvmpt4d.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
3		fvmpt4d.3	⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
4	1	fvmpt2f	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
5	3 2 4	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )