This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )