Theorem dffun5

Description: Alternate definition of function. (Contributed by NM, 29-Dec-1996)

	Ref	Expression
Assertion	dffun5	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge \forall x\exists z\forall y\left(⟨x,y⟩\in A\to y=z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dffun3	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge \forall x\exists z\forall y\left(xAy\to y=z\right)\right)$$
2		df-br	$$⊢xAy\leftrightarrow ⟨x,y⟩\in A$$
3	2	imbi1i	$$⊢\left(xAy\to y=z\right)\leftrightarrow \left(⟨x,y⟩\in A\to y=z\right)$$
4	3	albii	$$⊢\forall y\left(xAy\to y=z\right)\leftrightarrow \forall y\left(⟨x,y⟩\in A\to y=z\right)$$
5	4	exbii	$$⊢\exists z\forall y\left(xAy\to y=z\right)\leftrightarrow \exists z\forall y\left(⟨x,y⟩\in A\to y=z\right)$$
6	5	albii	$$⊢\forall x\exists z\forall y\left(xAy\to y=z\right)\leftrightarrow \forall x\exists z\forall y\left(⟨x,y⟩\in A\to y=z\right)$$
7	6	anbi2i	$$⊢\left(\mathrm{Rel}A\wedge \forall x\exists z\forall y\left(xAy\to y=z\right)\right)\leftrightarrow \left(\mathrm{Rel}A\wedge \forall x\exists z\forall y\left(⟨x,y⟩\in A\to y=z\right)\right)$$
8	1 7	bitri	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge \forall x\exists z\forall y\left(⟨x,y⟩\in A\to y=z\right)\right)$$