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		vex	$$⊢z\in \mathrm{V}$$
6	5	unisn	$$⊢\bigcup \left\{z\right\}=z$$
7	4 6	eqtr2di	$$⊢\left\{y|\phi \right\}=\left\{z\right\}\to z=\bigcup \left\{y|\phi \right\}$$
8	3 7	mpg	$$⊢{\exists }^{*}z\left\{y|\phi \right\}=\left\{z\right\}$$
9		nfv	$$⊢Ⅎz\left\{y|\phi \right\}=\left\{y\right\}$$
10		nfab1	$$⊢\underset{\_}{Ⅎ}y\left\{y|\phi \right\}$$
11	10	nfeq1	$$⊢Ⅎy\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\}\leftrightarrow \left\{y|\phi \right\}=\left\{z\right\}\right)$$
14	9 11 13	cbvmow	$$⊢{\exists }^{*}y\left\{y|\phi \right\}=\left\{y\right\}\leftrightarrow {\exists }^{*}z\left\{y|\phi \right\}=\left\{z\right\}$$
15	8 14	mpbir	$$⊢{\exists }^{*}y\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\leftrightarrow \mathrm{Fun}\left\{⟨x,y⟩|\left\{y|\phi \right\}=\left\{y\right\}\right\}$$
18	16 17	mpbir	$$⊢\mathrm{Fun}F$$