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\}\leftrightarrow \forall x{\exists }^{*}y\left\{y|\phi \right\}=\left\{y\right\}$$
3		mo2icl	$$⊢\forall z\left(\left\{y|\phi \right\}=\left\{z\right\}\to z=\bigcup \left\{y|\phi \right\}\right)\to {\exists }^{*}z\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		unisnv	$$⊢\bigcup \left\{z\right\}=z$$
6	4 5	eqtr2di	$$⊢\left\{y|\phi \right\}=\left\{z\right\}\to z=\bigcup \left\{y|\phi \right\}$$
7	3 6	mpg	$$⊢{\exists }^{*}z\left\{y|\phi \right\}=\left\{z\right\}$$
8		nfv	$$⊢Ⅎz\left\{y|\phi \right\}=\left\{y\right\}$$
9		nfab1	$$⊢\underset{\_}{Ⅎ}y\left\{y|\phi \right\}$$
10	9	nfeq1	$$⊢Ⅎy\left\{y|\phi \right\}=\left\{z\right\}$$
11		sneq	$$⊢y=z\to \left\{y\right\}=\left\{z\right\}$$
12	11	eqeq2d	$$⊢y=z\to \left(\left\{y|\phi \right\}=\left\{y\right\}\leftrightarrow \left\{y|\phi \right\}=\left\{z\right\}\right)$$
13	8 10 12	cbvmow	$$⊢{\exists }^{*}y\left\{y|\phi \right\}=\left\{y\right\}\leftrightarrow {\exists }^{*}z\left\{y|\phi \right\}=\left\{z\right\}$$
14	7 13	mpbir	$$⊢{\exists }^{*}y\left\{y|\phi \right\}=\left\{y\right\}$$
15	2 14	mpgbir	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\left\{y|\phi \right\}=\left\{y\right\}\right\}$$
16	1	funeqi	$$⊢\mathrm{Fun}F\leftrightarrow \mathrm{Fun}\left\{⟨x,y⟩|\left\{y|\phi \right\}=\left\{y\right\}\right\}$$
17	15 16	mpbir	$$⊢\mathrm{Fun}F$$