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