Theorem fnopabg

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004) (Proof shortened by Mario Carneiro, 4-Dec-2016)

	Ref	Expression
Hypothesis	fnopabg.1	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
Assertion	fnopabg	$$⊢\forall x\in A\exists !y\phi \leftrightarrow FFnA$$

Proof

Step	Hyp	Ref	Expression
1		fnopabg.1	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
2		moanimv	$$⊢{\exists }^{*}y\left(x\in A\wedge \phi \right)\leftrightarrow \left(x\in A\to {\exists }^{*}y\phi \right)$$
3	2	albii	$$⊢\forall x{\exists }^{*}y\left(x\in A\wedge \phi \right)\leftrightarrow \forall x\left(x\in A\to {\exists }^{*}y\phi \right)$$
4		funopab	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\leftrightarrow \forall x{\exists }^{*}y\left(x\in A\wedge \phi \right)$$
5		df-ral	$$⊢\forall x\in A{\exists }^{*}y\phi \leftrightarrow \forall x\left(x\in A\to {\exists }^{*}y\phi \right)$$
6	3 4 5	3bitr4ri	$$⊢\forall x\in A{\exists }^{*}y\phi \leftrightarrow \mathrm{Fun}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
7		dmopab3	$$⊢\forall x\in A\exists y\phi \leftrightarrow \mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}=A$$
8	6 7	anbi12i	$$⊢\left(\forall x\in A{\exists }^{*}y\phi \wedge \forall x\in A\exists y\phi \right)\leftrightarrow \left(\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\wedge \mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}=A\right)$$
9		r19.26	$$⊢\forall x\in A\left({\exists }^{*}y\phi \wedge \exists y\phi \right)\leftrightarrow \left(\forall x\in A{\exists }^{*}y\phi \wedge \forall x\in A\exists y\phi \right)$$
10		df-fn	$$⊢\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}FnA\leftrightarrow \left(\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\wedge \mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}=A\right)$$
11	8 9 10	3bitr4i	$$⊢\forall x\in A\left({\exists }^{*}y\phi \wedge \exists y\phi \right)\leftrightarrow \left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}FnA$$
12		df-eu	$$⊢\exists !y\phi \leftrightarrow \left(\exists y\phi \wedge {\exists }^{*}y\phi \right)$$
13	12	biancomi	$$⊢\exists !y\phi \leftrightarrow \left({\exists }^{*}y\phi \wedge \exists y\phi \right)$$
14	13	ralbii	$$⊢\forall x\in A\exists !y\phi \leftrightarrow \forall x\in A\left({\exists }^{*}y\phi \wedge \exists y\phi \right)$$
15	1	fneq1i	$$⊢FFnA\leftrightarrow \left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}FnA$$
16	11 14 15	3bitr4i	$$⊢\forall x\in A\exists !y\phi \leftrightarrow FFnA$$