Theorem dff13f

Description: A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of Monk1 p. 43. (Contributed by NM, 31-Jul-2003)

	Ref	Expression
Hypotheses	dff13f.1	$$⊢\underset{\_}{Ⅎ}xF$$
	dff13f.2	$$⊢\underset{\_}{Ⅎ}yF$$
Assertion	dff13f	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dff13f.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		dff13f.2	$$⊢\underset{\_}{Ⅎ}yF$$
3		dff13	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall w\in A\forall v\in A\left(F\left(w\right)=F\left(v\right)\to w=v\right)\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yw$$
5	2 4	nffv	$$⊢\underset{\_}{Ⅎ}yF\left(w\right)$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}yv$$
7	2 6	nffv	$$⊢\underset{\_}{Ⅎ}yF\left(v\right)$$
8	5 7	nfeq	$$⊢ℲyF\left(w\right)=F\left(v\right)$$
9		nfv	$$⊢Ⅎyw=v$$
10	8 9	nfim	$$⊢Ⅎy\left(F\left(w\right)=F\left(v\right)\to w=v\right)$$
11		nfv	$$⊢Ⅎv\left(F\left(w\right)=F\left(y\right)\to w=y\right)$$
12		fveq2	$$⊢v=y\to F\left(v\right)=F\left(y\right)$$
13	12	eqeq2d	$$⊢v=y\to \left(F\left(w\right)=F\left(v\right)\leftrightarrow F\left(w\right)=F\left(y\right)\right)$$
14		equequ2	$$⊢v=y\to \left(w=v\leftrightarrow w=y\right)$$
15	13 14	imbi12d	$$⊢v=y\to \left(\left(F\left(w\right)=F\left(v\right)\to w=v\right)\leftrightarrow \left(F\left(w\right)=F\left(y\right)\to w=y\right)\right)$$
16	10 11 15	cbvralw	$$⊢\forall v\in A\left(F\left(w\right)=F\left(v\right)\to w=v\right)\leftrightarrow \forall y\in A\left(F\left(w\right)=F\left(y\right)\to w=y\right)$$
17	16	ralbii	$$⊢\forall w\in A\forall v\in A\left(F\left(w\right)=F\left(v\right)\to w=v\right)\leftrightarrow \forall w\in A\forall y\in A\left(F\left(w\right)=F\left(y\right)\to w=y\right)$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
20	1 19	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(w\right)$$
21		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
22	1 21	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(y\right)$$
23	20 22	nfeq	$$⊢ℲxF\left(w\right)=F\left(y\right)$$
24		nfv	$$⊢Ⅎxw=y$$
25	23 24	nfim	$$⊢Ⅎx\left(F\left(w\right)=F\left(y\right)\to w=y\right)$$
26	18 25	nfralw	$$⊢Ⅎx\forall y\in A\left(F\left(w\right)=F\left(y\right)\to w=y\right)$$
27		nfv	$$⊢Ⅎw\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
28		fveqeq2	$$⊢w=x\to \left(F\left(w\right)=F\left(y\right)\leftrightarrow F\left(x\right)=F\left(y\right)\right)$$
29		equequ1	$$⊢w=x\to \left(w=y\leftrightarrow x=y\right)$$
30	28 29	imbi12d	$$⊢w=x\to \left(\left(F\left(w\right)=F\left(y\right)\to w=y\right)\leftrightarrow \left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
31	30	ralbidv	$$⊢w=x\to \left(\forall y\in A\left(F\left(w\right)=F\left(y\right)\to w=y\right)\leftrightarrow \forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
32	26 27 31	cbvralw	$$⊢\forall w\in A\forall y\in A\left(F\left(w\right)=F\left(y\right)\to w=y\right)\leftrightarrow \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
33	17 32	bitri	$$⊢\forall w\in A\forall v\in A\left(F\left(w\right)=F\left(v\right)\to w=v\right)\leftrightarrow \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
34	33	anbi2i	$$⊢\left(F:A⟶B\wedge \forall w\in A\forall v\in A\left(F\left(w\right)=F\left(v\right)\to w=v\right)\right)\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
35	3 34	bitri	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$