Description: Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | fvmpt4 | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) | |
2 | 1 | fvmpt2 | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 ) |