Step | Hyp | Ref
| Expression |
1 | | sneq 4526 |
. . . . . 6
⊢ (𝑥 = 𝐵 → {𝑥} = {𝐵}) |
2 | 1 | reseq2d 5825 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐹 ↾ {𝑥}) = (𝐹 ↾ {𝐵})) |
3 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
4 | | opeq12 4763 |
. . . . . . 7
⊢ ((𝑥 = 𝐵 ∧ (𝐹‘𝑥) = (𝐹‘𝐵)) → 〈𝑥, (𝐹‘𝑥)〉 = 〈𝐵, (𝐹‘𝐵)〉) |
5 | 3, 4 | mpdan 687 |
. . . . . 6
⊢ (𝑥 = 𝐵 → 〈𝑥, (𝐹‘𝑥)〉 = 〈𝐵, (𝐹‘𝐵)〉) |
6 | 5 | sneqd 4528 |
. . . . 5
⊢ (𝑥 = 𝐵 → {〈𝑥, (𝐹‘𝑥)〉} = {〈𝐵, (𝐹‘𝐵)〉}) |
7 | 2, 6 | eqeq12d 2754 |
. . . 4
⊢ (𝑥 = 𝐵 → ((𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉} ↔ (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉})) |
8 | 7 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝐹 Fn 𝐴 → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) ↔ (𝐹 Fn 𝐴 → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}))) |
9 | | vex 3402 |
. . . . . . 7
⊢ 𝑥 ∈ V |
10 | 9 | snss 4674 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↔ {𝑥} ⊆ 𝐴) |
11 | | fnssres 6459 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ {𝑥} ⊆ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) |
12 | 10, 11 | sylan2b 597 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) |
13 | | dffn2 6506 |
. . . . . 6
⊢ ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (𝐹 ↾ {𝑥}):{𝑥}⟶V) |
14 | 9 | fsn2 6908 |
. . . . . 6
⊢ ((𝐹 ↾ {𝑥}):{𝑥}⟶V ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉})) |
15 | | fvex 6687 |
. . . . . . . 8
⊢ ((𝐹 ↾ {𝑥})‘𝑥) ∈ V |
16 | 15 | biantrur 534 |
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉})) |
17 | | vsnid 4553 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ {𝑥} |
18 | | fvres 6693 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥} → ((𝐹 ↾ {𝑥})‘𝑥) = (𝐹‘𝑥)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ {𝑥})‘𝑥) = (𝐹‘𝑥) |
20 | 19 | opeq2i 4765 |
. . . . . . . . 9
⊢
〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉 = 〈𝑥, (𝐹‘𝑥)〉 |
21 | 20 | sneqi 4527 |
. . . . . . . 8
⊢
{〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} = {〈𝑥, (𝐹‘𝑥)〉} |
22 | 21 | eqeq2i 2751 |
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
23 | 16, 22 | bitr3i 280 |
. . . . . 6
⊢ ((((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉}) ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
24 | 13, 14, 23 | 3bitri 300 |
. . . . 5
⊢ ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
25 | 12, 24 | sylib 221 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
26 | 25 | expcom 417 |
. . 3
⊢ (𝑥 ∈ 𝐴 → (𝐹 Fn 𝐴 → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉})) |
27 | 8, 26 | vtoclga 3478 |
. 2
⊢ (𝐵 ∈ 𝐴 → (𝐹 Fn 𝐴 → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉})) |
28 | 27 | impcom 411 |
1
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}) |