# Metamath Proof Explorer

## Theorem fvmptf

Description: Value of a function given by an ordered-pair class abstraction. This version of fvmptg uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses fvmptf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
fvmptf.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
fvmptf.3 ${⊢}{x}={A}\to {B}={C}$
fvmptf.4 ${⊢}{F}=\left({x}\in {D}⟼{B}\right)$
Assertion fvmptf ${⊢}\left({A}\in {D}\wedge {C}\in {V}\right)\to {F}\left({A}\right)={C}$

### Proof

Step Hyp Ref Expression
1 fvmptf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 fvmptf.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
3 fvmptf.3 ${⊢}{x}={A}\to {B}={C}$
4 fvmptf.4 ${⊢}{F}=\left({x}\in {D}⟼{B}\right)$
5 2 nfel1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{C}\in \mathrm{V}$
6 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {D}⟼{B}\right)$
7 4 6 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
8 7 1 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({A}\right)$
9 8 2 nfeq ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}\left({A}\right)={C}$
10 5 9 nfim ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({C}\in \mathrm{V}\to {F}\left({A}\right)={C}\right)$
11 3 eleq1d ${⊢}{x}={A}\to \left({B}\in \mathrm{V}↔{C}\in \mathrm{V}\right)$
12 fveq2 ${⊢}{x}={A}\to {F}\left({x}\right)={F}\left({A}\right)$
13 12 3 eqeq12d ${⊢}{x}={A}\to \left({F}\left({x}\right)={B}↔{F}\left({A}\right)={C}\right)$
14 11 13 imbi12d ${⊢}{x}={A}\to \left(\left({B}\in \mathrm{V}\to {F}\left({x}\right)={B}\right)↔\left({C}\in \mathrm{V}\to {F}\left({A}\right)={C}\right)\right)$
15 4 fvmpt2 ${⊢}\left({x}\in {D}\wedge {B}\in \mathrm{V}\right)\to {F}\left({x}\right)={B}$
16 15 ex ${⊢}{x}\in {D}\to \left({B}\in \mathrm{V}\to {F}\left({x}\right)={B}\right)$
17 1 10 14 16 vtoclgaf ${⊢}{A}\in {D}\to \left({C}\in \mathrm{V}\to {F}\left({A}\right)={C}\right)$
18 elex ${⊢}{C}\in {V}\to {C}\in \mathrm{V}$
19 17 18 impel ${⊢}\left({A}\in {D}\wedge {C}\in {V}\right)\to {F}\left({A}\right)={C}$