# Metamath Proof Explorer

## Theorem nfmpt

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013)

Ref Expression
Hypotheses nfmpt.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfmpt.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfmpt ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}⟼{B}\right)$

### Proof

Step Hyp Ref Expression
1 nfmpt.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfmpt.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 df-mpt ${⊢}\left({y}\in {A}⟼{B}\right)=\left\{⟨{y},{z}⟩|\left({y}\in {A}\wedge {z}={B}\right)\right\}$
4 1 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
5 2 nfeq2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}={B}$
6 4 5 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {z}={B}\right)$
7 6 nfopab ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{⟨{y},{z}⟩|\left({y}\in {A}\wedge {z}={B}\right)\right\}$
8 3 7 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}⟼{B}\right)$