Step | Hyp | Ref
| Expression |
1 | | sneq 3744 |
. . . . . 6
⊢ (x = B →
{x} = {B}) |
2 | 1 | reseq2d 4934 |
. . . . 5
⊢ (x = B →
(F ↾
{x}) = (F ↾ {B})) |
3 | | fveq2 5328 |
. . . . . . 7
⊢ (x = B →
(F ‘x) = (F
‘B)) |
4 | | opeq12 4580 |
. . . . . . 7
⊢ ((x = B ∧ (F
‘x) = (F ‘B))
→ 〈x, (F
‘x)〉 = 〈B, (F
‘B)〉) |
5 | 3, 4 | mpdan 649 |
. . . . . 6
⊢ (x = B →
〈x,
(F ‘x)〉 = 〈B, (F ‘B)〉) |
6 | 5 | sneqd 3746 |
. . . . 5
⊢ (x = B →
{〈x,
(F ‘x)〉} = {〈B, (F ‘B)〉}) |
7 | 2, 6 | eqeq12d 2367 |
. . . 4
⊢ (x = B →
((F ↾
{x}) = {〈x, (F ‘x)〉} ↔ (F
↾ {B}) =
{〈B,
(F ‘B)〉})) |
8 | 7 | imbi2d 307 |
. . 3
⊢ (x = B →
((F Fn A → (F
↾ {x}) =
{〈x,
(F ‘x)〉}) ↔
(F Fn A
→ (F ↾ {B}) =
{〈B,
(F ‘B)〉}))) |
9 | | vex 2862 |
. . . . . . 7
⊢ x ∈
V |
10 | 9 | snss 3838 |
. . . . . 6
⊢ (x ∈ A ↔ {x}
⊆ A) |
11 | | fnssres 5196 |
. . . . . 6
⊢ ((F Fn A ∧ {x} ⊆ A) →
(F ↾
{x}) Fn {x}) |
12 | 10, 11 | sylan2b 461 |
. . . . 5
⊢ ((F Fn A ∧ x ∈ A) →
(F ↾
{x}) Fn {x}) |
13 | | dffn2 5224 |
. . . . . 6
⊢ ((F ↾ {x}) Fn {x}
↔ (F ↾ {x}):{x}–→V) |
14 | 9 | fsn2 5434 |
. . . . . 6
⊢ ((F ↾ {x}):{x}–→V ↔ (((F ↾ {x}) ‘x)
∈ V ∧
(F ↾
{x}) = {〈x, ((F ↾ {x}) ‘x)〉})) |
15 | | fvex 5339 |
. . . . . . . 8
⊢ ((F ↾ {x}) ‘x)
∈ V |
16 | 15 | biantrur 492 |
. . . . . . 7
⊢ ((F ↾ {x}) = {〈x, ((F ↾ {x})
‘x)〉} ↔ (((F
↾ {x})
‘x) ∈ V ∧ (F ↾ {x}) = {〈x, ((F ↾ {x})
‘x)〉})) |
17 | 9 | snid 3760 |
. . . . . . . . . . 11
⊢ x ∈ {x} |
18 | | fvres 5342 |
. . . . . . . . . . 11
⊢ (x ∈ {x} → ((F
↾ {x})
‘x) = (F ‘x)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((F ↾ {x}) ‘x) =
(F ‘x) |
20 | 19 | opeq2i 4582 |
. . . . . . . . 9
⊢ 〈x, ((F ↾ {x}) ‘x)〉 = 〈x, (F ‘x)〉 |
21 | 20 | sneqi 3745 |
. . . . . . . 8
⊢ {〈x, ((F ↾ {x}) ‘x)〉} = {〈x, (F ‘x)〉} |
22 | 21 | eqeq2i 2363 |
. . . . . . 7
⊢ ((F ↾ {x}) = {〈x, ((F ↾ {x})
‘x)〉} ↔ (F
↾ {x}) =
{〈x,
(F ‘x)〉}) |
23 | 16, 22 | bitr3i 242 |
. . . . . 6
⊢ ((((F ↾ {x}) ‘x)
∈ V ∧
(F ↾
{x}) = {〈x, ((F ↾ {x}) ‘x)〉}) ↔
(F ↾
{x}) = {〈x, (F ‘x)〉}) |
24 | 13, 14, 23 | 3bitri 262 |
. . . . 5
⊢ ((F ↾ {x}) Fn {x}
↔ (F ↾ {x}) =
{〈x,
(F ‘x)〉}) |
25 | 12, 24 | sylib 188 |
. . . 4
⊢ ((F Fn A ∧ x ∈ A) →
(F ↾
{x}) = {〈x, (F ‘x)〉}) |
26 | 25 | expcom 424 |
. . 3
⊢ (x ∈ A → (F Fn
A → (F ↾ {x}) = {〈x, (F
‘x)〉})) |
27 | 8, 26 | vtoclga 2920 |
. 2
⊢ (B ∈ A → (F Fn
A → (F ↾ {B}) = {〈B, (F
‘B)〉})) |
28 | 27 | impcom 419 |
1
⊢ ((F Fn A ∧ B ∈ A) →
(F ↾
{B}) = {〈B, (F ‘B)〉}) |