Theorem dffun6f

Description: Definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 9-Mar-1995) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	dffun6f.1	$$⊢\underset{\_}{Ⅎ}xA$$
	dffun6f.2	$$⊢\underset{\_}{Ⅎ}yA$$
Assertion	dffun6f	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge \forall x{\exists }^{*}yxAy\right)$$

Proof

Step	Hyp	Ref	Expression
1		dffun6f.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		dffun6f.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		dffun3	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge \forall w\exists u\forall v\left(wAv\to v=u\right)\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yw$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}yv$$
6	4 2 5	nfbr	$$⊢ℲywAv$$
7		nfv	$$⊢ℲvwAy$$
8		breq2	$$⊢v=y\to \left(wAv\leftrightarrow wAy\right)$$
9	6 7 8	cbvmow	$$⊢{\exists }^{*}vwAv\leftrightarrow {\exists }^{*}ywAy$$
10	9	albii	$$⊢\forall w{\exists }^{*}vwAv\leftrightarrow \forall w{\exists }^{*}ywAy$$
11		dfmo	$$⊢{\exists }^{*}vwAv\leftrightarrow \exists u\forall v\left(wAv\to v=u\right)$$
12	11	albii	$$⊢\forall w{\exists }^{*}vwAv\leftrightarrow \forall w\exists u\forall v\left(wAv\to v=u\right)$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
15	13 1 14	nfbr	$$⊢ℲxwAy$$
16	15	nfmov	$$⊢Ⅎx{\exists }^{*}ywAy$$
17		nfv	$$⊢Ⅎw{\exists }^{*}yxAy$$
18		breq1	$$⊢w=x\to \left(wAy\leftrightarrow xAy\right)$$
19	18	mobidv	$$⊢w=x\to \left({\exists }^{*}ywAy\leftrightarrow {\exists }^{*}yxAy\right)$$
20	16 17 19	cbvalv1	$$⊢\forall w{\exists }^{*}ywAy\leftrightarrow \forall x{\exists }^{*}yxAy$$
21	10 12 20	3bitr3ri	$$⊢\forall x{\exists }^{*}yxAy\leftrightarrow \forall w\exists u\forall v\left(wAv\to v=u\right)$$
22	21	anbi2i	$$⊢\left(\mathrm{Rel}A\wedge \forall x{\exists }^{*}yxAy\right)\leftrightarrow \left(\mathrm{Rel}A\wedge \forall w\exists u\forall v\left(wAv\to v=u\right)\right)$$
23	3 22	bitr4i	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge \forall x{\exists }^{*}yxAy\right)$$