Step |
Hyp |
Ref |
Expression |
1 |
|
sneq |
⊢ ( 𝑥 = 𝐵 → { 𝑥 } = { 𝐵 } ) |
2 |
1
|
reseq2d |
⊢ ( 𝑥 = 𝐵 → ( 𝐹 ↾ { 𝑥 } ) = ( 𝐹 ↾ { 𝐵 } ) ) |
3 |
|
fveq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) ) |
4 |
|
opeq12 |
⊢ ( ( 𝑥 = 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) ) → 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 = 〈 𝐵 , ( 𝐹 ‘ 𝐵 ) 〉 ) |
5 |
3 4
|
mpdan |
⊢ ( 𝑥 = 𝐵 → 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 = 〈 𝐵 , ( 𝐹 ‘ 𝐵 ) 〉 ) |
6 |
5
|
sneqd |
⊢ ( 𝑥 = 𝐵 → { 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 } = { 〈 𝐵 , ( 𝐹 ‘ 𝐵 ) 〉 } ) |
7 |
2 6
|
eqeq12d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 } ↔ ( 𝐹 ↾ { 𝐵 } ) = { 〈 𝐵 , ( 𝐹 ‘ 𝐵 ) 〉 } ) ) |
8 |
7
|
imbi2d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 } ) ↔ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝐵 } ) = { 〈 𝐵 , ( 𝐹 ‘ 𝐵 ) 〉 } ) ) ) |
9 |
|
vex |
⊢ 𝑥 ∈ V |
10 |
9
|
snss |
⊢ ( 𝑥 ∈ 𝐴 ↔ { 𝑥 } ⊆ 𝐴 ) |
11 |
|
fnssres |
⊢ ( ( 𝐹 Fn 𝐴 ∧ { 𝑥 } ⊆ 𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } ) |
12 |
10 11
|
sylan2b |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } ) |
13 |
|
dffn2 |
⊢ ( ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } ↔ ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ V ) |
14 |
9
|
fsn2 |
⊢ ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ V ↔ ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) 〉 } ) ) |
15 |
|
fvex |
⊢ ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V |
16 |
15
|
biantrur |
⊢ ( ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) 〉 } ↔ ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) 〉 } ) ) |
17 |
|
vsnid |
⊢ 𝑥 ∈ { 𝑥 } |
18 |
|
fvres |
⊢ ( 𝑥 ∈ { 𝑥 } → ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) |
19 |
17 18
|
ax-mp |
⊢ ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) |
20 |
19
|
opeq2i |
⊢ 〈 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) 〉 = 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 |
21 |
20
|
sneqi |
⊢ { 〈 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) 〉 } = { 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 } |
22 |
21
|
eqeq2i |
⊢ ( ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) 〉 } ↔ ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 } ) |
23 |
16 22
|
bitr3i |
⊢ ( ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) 〉 } ) ↔ ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 } ) |
24 |
13 14 23
|
3bitri |
⊢ ( ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } ↔ ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 } ) |
25 |
12 24
|
sylib |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 } ) |
26 |
25
|
expcom |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝑥 } ) = { 〈 𝑥 , ( 𝐹 ‘ 𝑥 ) 〉 } ) ) |
27 |
8 26
|
vtoclga |
⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝐵 } ) = { 〈 𝐵 , ( 𝐹 ‘ 𝐵 ) 〉 } ) ) |
28 |
27
|
impcom |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝐵 } ) = { 〈 𝐵 , ( 𝐹 ‘ 𝐵 ) 〉 } ) |