Theorem funopab

Description: A class of ordered pairs is a function when there is at most one second member for each pair. (Contributed by NM, 16-May-1995)

	Ref	Expression
Assertion	funopab	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\phi \right\}\leftrightarrow \forall x{\exists }^{*}y\phi$$

Proof

Step	Hyp	Ref	Expression
1		relopabv	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|\phi \right\}$$
2		nfopab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨x,y⟩|\phi \right\}$$
3		nfopab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨x,y⟩|\phi \right\}$$
4	2 3	dffun6f	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\phi \right\}\leftrightarrow \left(\mathrm{Rel}\left\{⟨x,y⟩|\phi \right\}\wedge \forall x{\exists }^{*}yx\left\{⟨x,y⟩|\phi \right\}y\right)$$
5	1 4	mpbiran	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\phi \right\}\leftrightarrow \forall x{\exists }^{*}yx\left\{⟨x,y⟩|\phi \right\}y$$
6		df-br	$$⊢x\left\{⟨x,y⟩|\phi \right\}y\leftrightarrow ⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}$$
7		opabidw	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \phi$$
8	6 7	bitri	$$⊢x\left\{⟨x,y⟩|\phi \right\}y\leftrightarrow \phi$$
9	8	mobii	$$⊢{\exists }^{*}yx\left\{⟨x,y⟩|\phi \right\}y\leftrightarrow {\exists }^{*}y\phi$$
10	9	albii	$$⊢\forall x{\exists }^{*}yx\left\{⟨x,y⟩|\phi \right\}y\leftrightarrow \forall x{\exists }^{*}y\phi$$
11	5 10	bitri	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\phi \right\}\leftrightarrow \forall x{\exists }^{*}y\phi$$