Step | Hyp | Ref
| Expression |
1 | | sneq 4571 |
. . . . . 6
⊢ (𝑥 = 𝐵 → {𝑥} = {𝐵}) |
2 | 1 | reseq2d 5891 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐹 ↾ {𝑥}) = (𝐹 ↾ {𝐵})) |
3 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
4 | | opeq12 4806 |
. . . . . . 7
⊢ ((𝑥 = 𝐵 ∧ (𝐹‘𝑥) = (𝐹‘𝐵)) → 〈𝑥, (𝐹‘𝑥)〉 = 〈𝐵, (𝐹‘𝐵)〉) |
5 | 3, 4 | mpdan 684 |
. . . . . 6
⊢ (𝑥 = 𝐵 → 〈𝑥, (𝐹‘𝑥)〉 = 〈𝐵, (𝐹‘𝐵)〉) |
6 | 5 | sneqd 4573 |
. . . . 5
⊢ (𝑥 = 𝐵 → {〈𝑥, (𝐹‘𝑥)〉} = {〈𝐵, (𝐹‘𝐵)〉}) |
7 | 2, 6 | eqeq12d 2754 |
. . . 4
⊢ (𝑥 = 𝐵 → ((𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉} ↔ (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉})) |
8 | 7 | imbi2d 341 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝐹 Fn 𝐴 → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) ↔ (𝐹 Fn 𝐴 → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}))) |
9 | | vex 3436 |
. . . . . . 7
⊢ 𝑥 ∈ V |
10 | 9 | snss 4719 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↔ {𝑥} ⊆ 𝐴) |
11 | | fnssres 6555 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ {𝑥} ⊆ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) |
12 | 10, 11 | sylan2b 594 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) |
13 | | dffn2 6602 |
. . . . . 6
⊢ ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (𝐹 ↾ {𝑥}):{𝑥}⟶V) |
14 | 9 | fsn2 7008 |
. . . . . 6
⊢ ((𝐹 ↾ {𝑥}):{𝑥}⟶V ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉})) |
15 | | fvex 6787 |
. . . . . . . 8
⊢ ((𝐹 ↾ {𝑥})‘𝑥) ∈ V |
16 | 15 | biantrur 531 |
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉})) |
17 | | vsnid 4598 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ {𝑥} |
18 | | fvres 6793 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥} → ((𝐹 ↾ {𝑥})‘𝑥) = (𝐹‘𝑥)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ {𝑥})‘𝑥) = (𝐹‘𝑥) |
20 | 19 | opeq2i 4808 |
. . . . . . . . 9
⊢
〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉 = 〈𝑥, (𝐹‘𝑥)〉 |
21 | 20 | sneqi 4572 |
. . . . . . . 8
⊢
{〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} = {〈𝑥, (𝐹‘𝑥)〉} |
22 | 21 | eqeq2i 2751 |
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
23 | 16, 22 | bitr3i 276 |
. . . . . 6
⊢ ((((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉}) ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
24 | 13, 14, 23 | 3bitri 297 |
. . . . 5
⊢ ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
25 | 12, 24 | sylib 217 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
26 | 25 | expcom 414 |
. . 3
⊢ (𝑥 ∈ 𝐴 → (𝐹 Fn 𝐴 → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉})) |
27 | 8, 26 | vtoclga 3513 |
. 2
⊢ (𝐵 ∈ 𝐴 → (𝐹 Fn 𝐴 → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉})) |
28 | 27 | impcom 408 |
1
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}) |