Theorem opabiota

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

	Ref	Expression
Hypotheses	opabiota.1	$$⊢F=\left\{⟨x,y⟩|\left\{y|\phi \right\}=\left\{y\right\}\right\}$$
	opabiota.2	$$⊢x=B\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	opabiota	$$⊢B\in \mathrm{dom}F\to F\left(B\right)=\left(\iota y|\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		opabiota.1	$$⊢F=\left\{⟨x,y⟩|\left\{y|\phi \right\}=\left\{y\right\}\right\}$$
2		opabiota.2	$$⊢x=B\to \left(\phi \leftrightarrow \psi \right)$$
3		fveq2	$$⊢x=B\to F\left(x\right)=F\left(B\right)$$
4	2	iotabidv	$$⊢x=B\to \left(\iota y|\phi \right)=\left(\iota y|\psi \right)$$
5	3 4	eqeq12d	$$⊢x=B\to \left(F\left(x\right)=\left(\iota y|\phi \right)\leftrightarrow F\left(B\right)=\left(\iota y|\psi \right)\right)$$
6		vex	$$⊢x\in \mathrm{V}$$
7	6	eldm	$$⊢x\in \mathrm{dom}F\leftrightarrow \exists yxFy$$
8		nfiota1	$$⊢\underset{\_}{Ⅎ}y\left(\iota y|\phi \right)$$
9	8	nfeq2	$$⊢ℲyF\left(x\right)=\left(\iota y|\phi \right)$$
10	1	opabiotafun	$$⊢\mathrm{Fun}F$$
11		funbrfv	$$⊢\mathrm{Fun}F\to \left(xFy\to F\left(x\right)=y\right)$$
12	10 11	ax-mp	$$⊢xFy\to F\left(x\right)=y$$
13		df-br	$$⊢xFy\leftrightarrow ⟨x,y⟩\in F$$
14	1	eleq2i	$$⊢⟨x,y⟩\in F\leftrightarrow ⟨x,y⟩\in \left\{⟨x,y⟩|\left\{y|\phi \right\}=\left\{y\right\}\right\}$$
15		opabidw	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\left\{y|\phi \right\}=\left\{y\right\}\right\}\leftrightarrow \left\{y|\phi \right\}=\left\{y\right\}$$
16	13 14 15	3bitri	$$⊢xFy\leftrightarrow \left\{y|\phi \right\}=\left\{y\right\}$$
17		vsnid	$$⊢y\in \left\{y\right\}$$
18		id	$$⊢\left\{y|\phi \right\}=\left\{y\right\}\to \left\{y|\phi \right\}=\left\{y\right\}$$
19	17 18	eleqtrrid	$$⊢\left\{y|\phi \right\}=\left\{y\right\}\to y\in \left\{y|\phi \right\}$$
20		abid	$$⊢y\in \left\{y|\phi \right\}\leftrightarrow \phi$$
21	19 20	sylib	$$⊢\left\{y|\phi \right\}=\left\{y\right\}\to \phi$$
22	16 21	sylbi	$$⊢xFy\to \phi$$
23		vex	$$⊢y\in \mathrm{V}$$
24	6 23	breldm	$$⊢xFy\to x\in \mathrm{dom}F$$
25	1	opabiotadm	$$⊢\mathrm{dom}F=\left\{x|\exists !y\phi \right\}$$
26	25	abeq2i	$$⊢x\in \mathrm{dom}F\leftrightarrow \exists !y\phi$$
27	24 26	sylib	$$⊢xFy\to \exists !y\phi$$
28		iota1	$$⊢\exists !y\phi \to \left(\phi \leftrightarrow \left(\iota y|\phi \right)=y\right)$$
29	27 28	syl	$$⊢xFy\to \left(\phi \leftrightarrow \left(\iota y|\phi \right)=y\right)$$
30	22 29	mpbid	$$⊢xFy\to \left(\iota y|\phi \right)=y$$
31	12 30	eqtr4d	$$⊢xFy\to F\left(x\right)=\left(\iota y|\phi \right)$$
32	9 31	exlimi	$$⊢\exists yxFy\to F\left(x\right)=\left(\iota y|\phi \right)$$
33	7 32	sylbi	$$⊢x\in \mathrm{dom}F\to F\left(x\right)=\left(\iota y|\phi \right)$$
34	5 33	vtoclga	$$⊢B\in \mathrm{dom}F\to F\left(B\right)=\left(\iota y|\psi \right)$$