Theorem dffun3f

Description: Alternate definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Emmett Weisz, 14-Mar-2021)

	Ref	Expression
Hypotheses	dffun3f.1	$$⊢\underset{\_}{Ⅎ}xA$$
	dffun3f.2	$$⊢\underset{\_}{Ⅎ}yA$$
	dffun3f.3	$$⊢\underset{\_}{Ⅎ}zA$$
Assertion	dffun3f	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge \forall x\exists z\forall y\left(xAy\to y=z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dffun3f.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		dffun3f.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		dffun3f.3	$$⊢\underset{\_}{Ⅎ}zA$$
4	1 2	dffun6f	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge \forall x{\exists }^{*}yxAy\right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}zx$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}zy$$
7	5 3 6	nfbr	$$⊢ℲzxAy$$
8	7	mof	$$⊢{\exists }^{*}yxAy\leftrightarrow \exists z\forall y\left(xAy\to y=z\right)$$
9	8	albii	$$⊢\forall x{\exists }^{*}yxAy\leftrightarrow \forall x\exists z\forall y\left(xAy\to y=z\right)$$
10	9	anbi2i	$$⊢\left(\mathrm{Rel}A\wedge \forall x{\exists }^{*}yxAy\right)\leftrightarrow \left(\mathrm{Rel}A\wedge \forall x\exists z\forall y\left(xAy\to y=z\right)\right)$$
11	4 10	bitri	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge \forall x\exists z\forall y\left(xAy\to y=z\right)\right)$$