Theorem fnressn 5270

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

Assertion

Ref	Expression
fnressn	⊢ ((𝐹 Fn A ∧ B ∈ A) → (𝐹 ↾ {B}) = {⟨B, (𝐹‘B)⟩})

Proof of Theorem fnressn

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sneq 3357	. . . . . 6 ⊢ (x = B → {x} = {B})
2	1	reseq2d 4535	. . . . 5 ⊢ (x = B → (𝐹 ↾ {x}) = (𝐹 ↾ {B}))
3		fveq2 5099	. . . . . . 7 ⊢ (x = B → (𝐹‘x) = (𝐹‘B))
4		opeq12 3521	. . . . . . 7 ⊢ ((x = B ∧ (𝐹‘x) = (𝐹‘B)) → ⟨x, (𝐹‘x)⟩ = ⟨B, (𝐹‘B)⟩)
5	3, 4	mpdan 400	. . . . . 6 ⊢ (x = B → ⟨x, (𝐹‘x)⟩ = ⟨B, (𝐹‘B)⟩)
6	5	sneqd 3359	. . . . 5 ⊢ (x = B → {⟨x, (𝐹‘x)⟩} = {⟨B, (𝐹‘B)⟩})
7	2, 6	eqeq12d 2032	. . . 4 ⊢ (x = B → ((𝐹 ↾ {x}) = {⟨x, (𝐹‘x)⟩} ↔ (𝐹 ↾ {B}) = {⟨B, (𝐹‘B)⟩}))
8	7	imbi2d 219	. . 3 ⊢ (x = B → ((𝐹 Fn A → (𝐹 ↾ {x}) = {⟨x, (𝐹‘x)⟩}) ↔ (𝐹 Fn A → (𝐹 ↾ {B}) = {⟨B, (𝐹‘B)⟩})))
9		vex 2534	. . . . . . 7 ⊢ x ∈ V
10	9	snss 3464	. . . . . 6 ⊢ (x ∈ A ↔ {x} ⊆ A)
11		fnssres 4934	. . . . . 6 ⊢ ((𝐹 Fn A ∧ {x} ⊆ A) → (𝐹 ↾ {x}) Fn {x})
12	10, 11	sylan2b 271	. . . . 5 ⊢ ((𝐹 Fn A ∧ x ∈ A) → (𝐹 ↾ {x}) Fn {x})
13		dffn2 4969	. . . . . . 7 ⊢ ((𝐹 ↾ {x}) Fn {x} ↔ (𝐹 ↾ {x}):{x}⟶V)
14	9	fsn2 5258	. . . . . . 7 ⊢ ((𝐹 ↾ {x}):{x}⟶V ↔ (((𝐹 ↾ {x})‘x) ∈ V ∧ (𝐹 ↾ {x}) = {⟨x, ((𝐹 ↾ {x})‘x)⟩}))
15	13, 14	bitri 173	. . . . . 6 ⊢ ((𝐹 ↾ {x}) Fn {x} ↔ (((𝐹 ↾ {x})‘x) ∈ V ∧ (𝐹 ↾ {x}) = {⟨x, ((𝐹 ↾ {x})‘x)⟩}))
16		ssnid 3374	. . . . . . . . . . 11 ⊢ x ∈ {x}
17		fvres 5119	. . . . . . . . . . 11 ⊢ (x ∈ {x} → ((𝐹 ↾ {x})‘x) = (𝐹‘x))
18	16, 17	ax-mp 7	. . . . . . . . . 10 ⊢ ((𝐹 ↾ {x})‘x) = (𝐹‘x)
19	18	opeq2i 3523	. . . . . . . . 9 ⊢ ⟨x, ((𝐹 ↾ {x})‘x)⟩ = ⟨x, (𝐹‘x)⟩
20	19	sneqi 3358	. . . . . . . 8 ⊢ {⟨x, ((𝐹 ↾ {x})‘x)⟩} = {⟨x, (𝐹‘x)⟩}
21	20	eqeq2i 2028	. . . . . . 7 ⊢ ((𝐹 ↾ {x}) = {⟨x, ((𝐹 ↾ {x})‘x)⟩} ↔ (𝐹 ↾ {x}) = {⟨x, (𝐹‘x)⟩})
22		snssi 3478	. . . . . . . . . 10 ⊢ (x ∈ A → {x} ⊆ A)
23	22, 11	sylan2 270	. . . . . . . . 9 ⊢ ((𝐹 Fn A ∧ x ∈ A) → (𝐹 ↾ {x}) Fn {x})
24		funfvex 5113	. . . . . . . . . 10 ⊢ ((Fun (𝐹 ↾ {x}) ∧ x ∈ dom (𝐹 ↾ {x})) → ((𝐹 ↾ {x})‘x) ∈ V)
25	24	funfni 4921	. . . . . . . . 9 ⊢ (((𝐹 ↾ {x}) Fn {x} ∧ x ∈ {x}) → ((𝐹 ↾ {x})‘x) ∈ V)
26	23, 16, 25	sylancl 394	. . . . . . . 8 ⊢ ((𝐹 Fn A ∧ x ∈ A) → ((𝐹 ↾ {x})‘x) ∈ V)
27	26	biantrurd 289	. . . . . . 7 ⊢ ((𝐹 Fn A ∧ x ∈ A) → ((𝐹 ↾ {x}) = {⟨x, ((𝐹 ↾ {x})‘x)⟩} ↔ (((𝐹 ↾ {x})‘x) ∈ V ∧ (𝐹 ↾ {x}) = {⟨x, ((𝐹 ↾ {x})‘x)⟩})))
28	21, 27	syl5rbbr 184	. . . . . 6 ⊢ ((𝐹 Fn A ∧ x ∈ A) → ((((𝐹 ↾ {x})‘x) ∈ V ∧ (𝐹 ↾ {x}) = {⟨x, ((𝐹 ↾ {x})‘x)⟩}) ↔ (𝐹 ↾ {x}) = {⟨x, (𝐹‘x)⟩}))
29	15, 28	syl5bb 181	. . . . 5 ⊢ ((𝐹 Fn A ∧ x ∈ A) → ((𝐹 ↾ {x}) Fn {x} ↔ (𝐹 ↾ {x}) = {⟨x, (𝐹‘x)⟩}))
30	12, 29	mpbid 135	. . . 4 ⊢ ((𝐹 Fn A ∧ x ∈ A) → (𝐹 ↾ {x}) = {⟨x, (𝐹‘x)⟩})
31	30	expcom 109	. . 3 ⊢ (x ∈ A → (𝐹 Fn A → (𝐹 ↾ {x}) = {⟨x, (𝐹‘x)⟩}))
32	8, 31	vtoclga 2592	. 2 ⊢ (B ∈ A → (𝐹 Fn A → (𝐹 ↾ {B}) = {⟨B, (𝐹‘B)⟩}))
33	32	impcom 116	1 ⊢ ((𝐹 Fn A ∧ B ∈ A) → (𝐹 ↾ {B}) = {⟨B, (𝐹‘B)⟩})

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1226   ∈ wcel 1370  Vcvv 2531   ⊆ wss 2890  {csn 3346  ⟨cop 3349   ↾ cres 4270   Fn wfn 4820  ⟶wf 4821  ‘cfv 4825

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-reu 2287  df-v 2533  df-sbc 2738  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fun 4827  df-fn 4828  df-f 4829  df-f1 4830  df-fo 4831  df-f1o 4832  df-fv 4833

This theorem is referenced by:  fressnfv  5271