Theorem fnressn

Description: A function restricted to a singleton. (Contributed by NM, 9-Oct-2004)

	Ref	Expression
Assertion	fnressn	$$⊢\left(FFnA\wedge B\in A\right)\to {F\upharpoonright }_{\left\{B\right\}}=\left\{⟨B,F\left(B\right)⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		sneq	$$⊢x=B\to \left\{x\right\}=\left\{B\right\}$$
2	1	reseq2d	$$⊢x=B\to {F\upharpoonright }_{\left\{x\right\}}={F\upharpoonright }_{\left\{B\right\}}$$
3		fveq2	$$⊢x=B\to F\left(x\right)=F\left(B\right)$$
4		opeq12	$$⊢\left(x=B\wedge F\left(x\right)=F\left(B\right)\right)\to ⟨x,F\left(x\right)⟩=⟨B,F\left(B\right)⟩$$
5	3 4	mpdan	$$⊢x=B\to ⟨x,F\left(x\right)⟩=⟨B,F\left(B\right)⟩$$
6	5	sneqd	$$⊢x=B\to \left\{⟨x,F\left(x\right)⟩\right\}=\left\{⟨B,F\left(B\right)⟩\right\}$$
7	2 6	eqeq12d	$$⊢x=B\to \left({F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,F\left(x\right)⟩\right\}\leftrightarrow {F\upharpoonright }_{\left\{B\right\}}=\left\{⟨B,F\left(B\right)⟩\right\}\right)$$
8	7	imbi2d	$$⊢x=B\to \left(\left(FFnA\to {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,F\left(x\right)⟩\right\}\right)\leftrightarrow \left(FFnA\to {F\upharpoonright }_{\left\{B\right\}}=\left\{⟨B,F\left(B\right)⟩\right\}\right)\right)$$
9		vex	$$⊢x\in \mathrm{V}$$
10	9	snss	$$⊢x\in A\leftrightarrow \left\{x\right\}\subseteq A$$
11		fnssres	$$⊢\left(FFnA\wedge \left\{x\right\}\subseteq A\right)\to \left({F\upharpoonright }_{\left\{x\right\}}\right)Fn\left\{x\right\}$$
12	10 11	sylan2b	$$⊢\left(FFnA\wedge x\in A\right)\to \left({F\upharpoonright }_{\left\{x\right\}}\right)Fn\left\{x\right\}$$
13		dffn2	$$⊢\left({F\upharpoonright }_{\left\{x\right\}}\right)Fn\left\{x\right\}\leftrightarrow \left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶\mathrm{V}$$
14	9	fsn2	$$⊢\left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶\mathrm{V}\leftrightarrow \left(\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)\in \mathrm{V}\wedge {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}\right)$$
15		fvex	$$⊢\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)\in \mathrm{V}$$
16	15	biantrur	$$⊢{F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}\leftrightarrow \left(\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)\in \mathrm{V}\wedge {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}\right)$$
17		vsnid	$$⊢x\in \left\{x\right\}$$
18		fvres	$$⊢x\in \left\{x\right\}\to \left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)=F\left(x\right)$$
19	17 18	ax-mp	$$⊢\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)=F\left(x\right)$$
20	19	opeq2i	$$⊢⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩=⟨x,F\left(x\right)⟩$$
21	20	sneqi	$$⊢\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}=\left\{⟨x,F\left(x\right)⟩\right\}$$
22	21	eqeq2i	$$⊢{F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}\leftrightarrow {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,F\left(x\right)⟩\right\}$$
23	16 22	bitr3i	$$⊢\left(\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)\in \mathrm{V}\wedge {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}\right)\leftrightarrow {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,F\left(x\right)⟩\right\}$$
24	13 14 23	3bitri	$$⊢\left({F\upharpoonright }_{\left\{x\right\}}\right)Fn\left\{x\right\}\leftrightarrow {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,F\left(x\right)⟩\right\}$$
25	12 24	sylib	$$⊢\left(FFnA\wedge x\in A\right)\to {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,F\left(x\right)⟩\right\}$$
26	25	expcom	$$⊢x\in A\to \left(FFnA\to {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,F\left(x\right)⟩\right\}\right)$$
27	8 26	vtoclga	$$⊢B\in A\to \left(FFnA\to {F\upharpoonright }_{\left\{B\right\}}=\left\{⟨B,F\left(B\right)⟩\right\}\right)$$
28	27	impcom	$$⊢\left(FFnA\wedge B\in A\right)\to {F\upharpoonright }_{\left\{B\right\}}=\left\{⟨B,F\left(B\right)⟩\right\}$$