Theorem fressnfv

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

	Ref	Expression
Assertion	fressnfv	$$⊢\left(FFnA\wedge B\in A\right)\to \left(\left({F\upharpoonright }_{\left\{B\right\}}\right):\left\{B\right\}⟶C\leftrightarrow F\left(B\right)\in C\right)$$

Proof

Step	Hyp	Ref	Expression
1		sneq	$$⊢x=B\to \left\{x\right\}=\left\{B\right\}$$
2		reseq2	$$⊢\left\{x\right\}=\left\{B\right\}\to {F\upharpoonright }_{\left\{x\right\}}={F\upharpoonright }_{\left\{B\right\}}$$
3	2	feq1d	$$⊢\left\{x\right\}=\left\{B\right\}\to \left(\left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶C\leftrightarrow \left({F\upharpoonright }_{\left\{B\right\}}\right):\left\{x\right\}⟶C\right)$$
4		feq2	$$⊢\left\{x\right\}=\left\{B\right\}\to \left(\left({F\upharpoonright }_{\left\{B\right\}}\right):\left\{x\right\}⟶C\leftrightarrow \left({F\upharpoonright }_{\left\{B\right\}}\right):\left\{B\right\}⟶C\right)$$
5	3 4	bitrd	$$⊢\left\{x\right\}=\left\{B\right\}\to \left(\left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶C\leftrightarrow \left({F\upharpoonright }_{\left\{B\right\}}\right):\left\{B\right\}⟶C\right)$$
6	1 5	syl	$$⊢x=B\to \left(\left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶C\leftrightarrow \left({F\upharpoonright }_{\left\{B\right\}}\right):\left\{B\right\}⟶C\right)$$
7		fveq2	$$⊢x=B\to F\left(x\right)=F\left(B\right)$$
8	7	eleq1d	$$⊢x=B\to \left(F\left(x\right)\in C\leftrightarrow F\left(B\right)\in C\right)$$
9	6 8	bibi12d	$$⊢x=B\to \left(\left(\left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶C\leftrightarrow F\left(x\right)\in C\right)\leftrightarrow \left(\left({F\upharpoonright }_{\left\{B\right\}}\right):\left\{B\right\}⟶C\leftrightarrow F\left(B\right)\in C\right)\right)$$
10	9	imbi2d	$$⊢x=B\to \left(\left(FFnA\to \left(\left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶C\leftrightarrow F\left(x\right)\in C\right)\right)\leftrightarrow \left(FFnA\to \left(\left({F\upharpoonright }_{\left\{B\right\}}\right):\left\{B\right\}⟶C\leftrightarrow F\left(B\right)\in C\right)\right)\right)$$
11		fnressn	$$⊢\left(FFnA\wedge x\in A\right)\to {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,F\left(x\right)⟩\right\}$$
12		vsnid	$$⊢x\in \left\{x\right\}$$
13		fvres	$$⊢x\in \left\{x\right\}\to \left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)=F\left(x\right)$$
14	12 13	ax-mp	$$⊢\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)=F\left(x\right)$$
15	14	opeq2i	$$⊢⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩=⟨x,F\left(x\right)⟩$$
16	15	sneqi	$$⊢\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}=\left\{⟨x,F\left(x\right)⟩\right\}$$
17	16	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\}$$
18		vex	$$⊢x\in \mathrm{V}$$
19	18	fsn2	$$⊢\left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶C\leftrightarrow \left(\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)\in C\wedge {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}\right)$$
20	14	eleq1i	$$⊢\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)\in C\leftrightarrow F\left(x\right)\in C$$
21		iba	$$⊢{F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}\to \left(\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)\in C\leftrightarrow \left(\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)\in C\wedge {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}\right)\right)$$
22	20 21	syl5rbbr	$$⊢{F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}\to \left(\left(\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)\in C\wedge {F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}\right)\leftrightarrow F\left(x\right)\in C\right)$$
23	19 22	syl5bb	$$⊢{F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,\left({F\upharpoonright }_{\left\{x\right\}}\right)\left(x\right)⟩\right\}\to \left(\left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶C\leftrightarrow F\left(x\right)\in C\right)$$
24	17 23	sylbir	$$⊢{F\upharpoonright }_{\left\{x\right\}}=\left\{⟨x,F\left(x\right)⟩\right\}\to \left(\left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶C\leftrightarrow F\left(x\right)\in C\right)$$
25	11 24	syl	$$⊢\left(FFnA\wedge x\in A\right)\to \left(\left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶C\leftrightarrow F\left(x\right)\in C\right)$$
26	25	expcom	$$⊢x\in A\to \left(FFnA\to \left(\left({F\upharpoonright }_{\left\{x\right\}}\right):\left\{x\right\}⟶C\leftrightarrow F\left(x\right)\in C\right)\right)$$
27	10 26	vtoclga	$$⊢B\in A\to \left(FFnA\to \left(\left({F\upharpoonright }_{\left\{B\right\}}\right):\left\{B\right\}⟶C\leftrightarrow F\left(B\right)\in C\right)\right)$$
28	27	impcom	$$⊢\left(FFnA\wedge B\in A\right)\to \left(\left({F\upharpoonright }_{\left\{B\right\}}\right):\left\{B\right\}⟶C\leftrightarrow F\left(B\right)\in C\right)$$