# Metamath Proof Explorer

## Theorem opabiotafun

Description: Define a function whose value is "the unique y such that ph ( x , y ) ". (Contributed by NM, 19-May-2015)

Ref Expression
Hypothesis opabiota.1 ${⊢}{F}=\left\{⟨{x},{y}⟩|\left\{{y}|{\phi }\right\}=\left\{{y}\right\}\right\}$
Assertion opabiotafun ${⊢}\mathrm{Fun}{F}$

### Proof

Step Hyp Ref Expression
1 opabiota.1 ${⊢}{F}=\left\{⟨{x},{y}⟩|\left\{{y}|{\phi }\right\}=\left\{{y}\right\}\right\}$
2 funopab ${⊢}\mathrm{Fun}\left\{⟨{x},{y}⟩|\left\{{y}|{\phi }\right\}=\left\{{y}\right\}\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{y}|{\phi }\right\}=\left\{{y}\right\}$
3 mo2icl ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left\{{y}|{\phi }\right\}=\left\{{z}\right\}\to {z}=\bigcup \left\{{y}|{\phi }\right\}\right)\to {\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}\left\{{y}|{\phi }\right\}=\left\{{z}\right\}$
4 unieq ${⊢}\left\{{y}|{\phi }\right\}=\left\{{z}\right\}\to \bigcup \left\{{y}|{\phi }\right\}=\bigcup \left\{{z}\right\}$
5 vex ${⊢}{z}\in \mathrm{V}$
6 5 unisn ${⊢}\bigcup \left\{{z}\right\}={z}$
7 4 6 syl6req ${⊢}\left\{{y}|{\phi }\right\}=\left\{{z}\right\}\to {z}=\bigcup \left\{{y}|{\phi }\right\}$
8 3 7 mpg ${⊢}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}\left\{{y}|{\phi }\right\}=\left\{{z}\right\}$
9 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left\{{y}|{\phi }\right\}=\left\{{y}\right\}$
10 nfab1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{{y}|{\phi }\right\}$
11 10 nfeq1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left\{{y}|{\phi }\right\}=\left\{{z}\right\}$
12 sneq ${⊢}{y}={z}\to \left\{{y}\right\}=\left\{{z}\right\}$
13 12 eqeq2d ${⊢}{y}={z}\to \left(\left\{{y}|{\phi }\right\}=\left\{{y}\right\}↔\left\{{y}|{\phi }\right\}=\left\{{z}\right\}\right)$
14 9 11 13 cbvmow ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{y}|{\phi }\right\}=\left\{{y}\right\}↔{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}\left\{{y}|{\phi }\right\}=\left\{{z}\right\}$
15 8 14 mpbir ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{y}|{\phi }\right\}=\left\{{y}\right\}$
16 2 15 mpgbir ${⊢}\mathrm{Fun}\left\{⟨{x},{y}⟩|\left\{{y}|{\phi }\right\}=\left\{{y}\right\}\right\}$
17 1 funeqi ${⊢}\mathrm{Fun}{F}↔\mathrm{Fun}\left\{⟨{x},{y}⟩|\left\{{y}|{\phi }\right\}=\left\{{y}\right\}\right\}$
18 16 17 mpbir ${⊢}\mathrm{Fun}{F}$