# Metamath Proof Explorer

## Theorem mptfng

Description: The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011)

Ref Expression
Hypothesis mptfng.1 ${⊢}{F}=\left({x}\in {A}⟼{B}\right)$
Assertion mptfng ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{V}↔{F}Fn{A}$

### Proof

Step Hyp Ref Expression
1 mptfng.1 ${⊢}{F}=\left({x}\in {A}⟼{B}\right)$
2 eueq ${⊢}{B}\in \mathrm{V}↔\exists !{y}\phantom{\rule{.4em}{0ex}}{y}={B}$
3 2 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{V}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{y}={B}$
4 df-mpt ${⊢}\left({x}\in {A}⟼{B}\right)=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}={B}\right)\right\}$
5 1 4 eqtri ${⊢}{F}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}={B}\right)\right\}$
6 5 fnopabg ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{y}={B}↔{F}Fn{A}$
7 3 6 bitri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{V}↔{F}Fn{A}$