| Step | Hyp | Ref
 | Expression | 
| 1 |   | sneq 3633 | 
. . . . . 6
⊢ (𝑥 = 𝐵 → {𝑥} = {𝐵}) | 
| 2 | 1 | reseq2d 4946 | 
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐹 ↾ {𝑥}) = (𝐹 ↾ {𝐵})) | 
| 3 |   | fveq2 5558 | 
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) | 
| 4 |   | opeq12 3810 | 
. . . . . . 7
⊢ ((𝑥 = 𝐵 ∧ (𝐹‘𝑥) = (𝐹‘𝐵)) → 〈𝑥, (𝐹‘𝑥)〉 = 〈𝐵, (𝐹‘𝐵)〉) | 
| 5 | 3, 4 | mpdan 421 | 
. . . . . 6
⊢ (𝑥 = 𝐵 → 〈𝑥, (𝐹‘𝑥)〉 = 〈𝐵, (𝐹‘𝐵)〉) | 
| 6 | 5 | sneqd 3635 | 
. . . . 5
⊢ (𝑥 = 𝐵 → {〈𝑥, (𝐹‘𝑥)〉} = {〈𝐵, (𝐹‘𝐵)〉}) | 
| 7 | 2, 6 | eqeq12d 2211 | 
. . . 4
⊢ (𝑥 = 𝐵 → ((𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉} ↔ (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉})) | 
| 8 | 7 | imbi2d 230 | 
. . 3
⊢ (𝑥 = 𝐵 → ((𝐹 Fn 𝐴 → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) ↔ (𝐹 Fn 𝐴 → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}))) | 
| 9 |   | vex 2766 | 
. . . . . . 7
⊢ 𝑥 ∈ V | 
| 10 | 9 | snss 3757 | 
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↔ {𝑥} ⊆ 𝐴) | 
| 11 |   | fnssres 5371 | 
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ {𝑥} ⊆ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) | 
| 12 | 10, 11 | sylan2b 287 | 
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) | 
| 13 |   | dffn2 5409 | 
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (𝐹 ↾ {𝑥}):{𝑥}⟶V) | 
| 14 | 9 | fsn2 5736 | 
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}):{𝑥}⟶V ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉})) | 
| 15 | 13, 14 | bitri 184 | 
. . . . . 6
⊢ ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉})) | 
| 16 |   | snssi 3766 | 
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ 𝐴) | 
| 17 | 16, 11 | sylan2 286 | 
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) | 
| 18 |   | vsnid 3654 | 
. . . . . . . . 9
⊢ 𝑥 ∈ {𝑥} | 
| 19 |   | funfvex 5575 | 
. . . . . . . . . 10
⊢ ((Fun
(𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom (𝐹 ↾ {𝑥})) → ((𝐹 ↾ {𝑥})‘𝑥) ∈ V) | 
| 20 | 19 | funfni 5358 | 
. . . . . . . . 9
⊢ (((𝐹 ↾ {𝑥}) Fn {𝑥} ∧ 𝑥 ∈ {𝑥}) → ((𝐹 ↾ {𝑥})‘𝑥) ∈ V) | 
| 21 | 17, 18, 20 | sylancl 413 | 
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹 ↾ {𝑥})‘𝑥) ∈ V) | 
| 22 | 21 | biantrurd 305 | 
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉}))) | 
| 23 |   | fvres 5582 | 
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥} → ((𝐹 ↾ {𝑥})‘𝑥) = (𝐹‘𝑥)) | 
| 24 | 18, 23 | ax-mp 5 | 
. . . . . . . . . 10
⊢ ((𝐹 ↾ {𝑥})‘𝑥) = (𝐹‘𝑥) | 
| 25 | 24 | opeq2i 3812 | 
. . . . . . . . 9
⊢
〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉 = 〈𝑥, (𝐹‘𝑥)〉 | 
| 26 | 25 | sneqi 3634 | 
. . . . . . . 8
⊢
{〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} = {〈𝑥, (𝐹‘𝑥)〉} | 
| 27 | 26 | eqeq2i 2207 | 
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) | 
| 28 | 22, 27 | bitr3di 195 | 
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉}) ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉})) | 
| 29 | 15, 28 | bitrid 192 | 
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉})) | 
| 30 | 12, 29 | mpbid 147 | 
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) | 
| 31 | 30 | expcom 116 | 
. . 3
⊢ (𝑥 ∈ 𝐴 → (𝐹 Fn 𝐴 → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉})) | 
| 32 | 8, 31 | vtoclga 2830 | 
. 2
⊢ (𝐵 ∈ 𝐴 → (𝐹 Fn 𝐴 → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉})) | 
| 33 | 32 | impcom 125 | 
1
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}) |