# Metamath Proof Explorer

## Theorem fvmptg

Description: Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses fvmptg.1 ${⊢}{x}={A}\to {B}={C}$
fvmptg.2 ${⊢}{F}=\left({x}\in {D}⟼{B}\right)$
Assertion fvmptg ${⊢}\left({A}\in {D}\wedge {C}\in {R}\right)\to {F}\left({A}\right)={C}$

### Proof

Step Hyp Ref Expression
1 fvmptg.1 ${⊢}{x}={A}\to {B}={C}$
2 fvmptg.2 ${⊢}{F}=\left({x}\in {D}⟼{B}\right)$
3 eqid ${⊢}{C}={C}$
4 1 eqeq2d ${⊢}{x}={A}\to \left({y}={B}↔{y}={C}\right)$
5 eqeq1 ${⊢}{y}={C}\to \left({y}={C}↔{C}={C}\right)$
6 moeq ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{y}={B}$
7 6 a1i ${⊢}{x}\in {D}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{y}={B}$
8 df-mpt ${⊢}\left({x}\in {D}⟼{B}\right)=\left\{⟨{x},{y}⟩|\left({x}\in {D}\wedge {y}={B}\right)\right\}$
9 2 8 eqtri ${⊢}{F}=\left\{⟨{x},{y}⟩|\left({x}\in {D}\wedge {y}={B}\right)\right\}$
10 4 5 7 9 fvopab3ig ${⊢}\left({A}\in {D}\wedge {C}\in {R}\right)\to \left({C}={C}\to {F}\left({A}\right)={C}\right)$
11 3 10 mpi ${⊢}\left({A}\in {D}\wedge {C}\in {R}\right)\to {F}\left({A}\right)={C}$