Step | Hyp | Ref
| Expression |
1 | | df-dfat 41196 |
. 2
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) |
2 | | relres 5426 |
. . . 4
⊢ Rel
(𝐹 ↾ {𝐴}) |
3 | | dffun8 5916 |
. . . 4
⊢ (Fun
(𝐹 ↾ {𝐴}) ↔ (Rel (𝐹 ↾ {𝐴}) ∧ ∀𝑥 ∈ dom (𝐹 ↾ {𝐴})∃!𝑦 𝑥(𝐹 ↾ {𝐴})𝑦)) |
4 | 2, 3 | mpbiran 953 |
. . 3
⊢ (Fun
(𝐹 ↾ {𝐴}) ↔ ∀𝑥 ∈ dom (𝐹 ↾ {𝐴})∃!𝑦 𝑥(𝐹 ↾ {𝐴})𝑦) |
5 | 4 | anbi2i 730 |
. 2
⊢ ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ↔ (𝐴 ∈ dom 𝐹 ∧ ∀𝑥 ∈ dom (𝐹 ↾ {𝐴})∃!𝑦 𝑥(𝐹 ↾ {𝐴})𝑦)) |
6 | | vex 3203 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
7 | 6 | brres 5402 |
. . . . . . 7
⊢ (𝑥(𝐹 ↾ {𝐴})𝑦 ↔ (𝑥𝐹𝑦 ∧ 𝑥 ∈ {𝐴})) |
8 | 7 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ dom 𝐹 → (𝑥(𝐹 ↾ {𝐴})𝑦 ↔ (𝑥𝐹𝑦 ∧ 𝑥 ∈ {𝐴}))) |
9 | 8 | eubidv 2490 |
. . . . 5
⊢ (𝐴 ∈ dom 𝐹 → (∃!𝑦 𝑥(𝐹 ↾ {𝐴})𝑦 ↔ ∃!𝑦(𝑥𝐹𝑦 ∧ 𝑥 ∈ {𝐴}))) |
10 | 9 | ralbidv 2986 |
. . . 4
⊢ (𝐴 ∈ dom 𝐹 → (∀𝑥 ∈ dom (𝐹 ↾ {𝐴})∃!𝑦 𝑥(𝐹 ↾ {𝐴})𝑦 ↔ ∀𝑥 ∈ dom (𝐹 ↾ {𝐴})∃!𝑦(𝑥𝐹𝑦 ∧ 𝑥 ∈ {𝐴}))) |
11 | | eldmressnsn 5439 |
. . . . 5
⊢ (𝐴 ∈ dom 𝐹 → 𝐴 ∈ dom (𝐹 ↾ {𝐴})) |
12 | | eldmressn 41203 |
. . . . 5
⊢ (𝑥 ∈ dom (𝐹 ↾ {𝐴}) → 𝑥 = 𝐴) |
13 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥𝐹𝑦 ↔ 𝐴𝐹𝑦)) |
14 | 13 | anbi1d 741 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑥𝐹𝑦 ∧ 𝑥 ∈ {𝐴}) ↔ (𝐴𝐹𝑦 ∧ 𝑥 ∈ {𝐴}))) |
15 | | velsn 4193 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
16 | 15 | biimpri 218 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → 𝑥 ∈ {𝐴}) |
17 | 16 | biantrud 528 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐴𝐹𝑦 ↔ (𝐴𝐹𝑦 ∧ 𝑥 ∈ {𝐴}))) |
18 | 14, 17 | bitr4d 271 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑥𝐹𝑦 ∧ 𝑥 ∈ {𝐴}) ↔ 𝐴𝐹𝑦)) |
19 | 18 | eubidv 2490 |
. . . . 5
⊢ (𝑥 = 𝐴 → (∃!𝑦(𝑥𝐹𝑦 ∧ 𝑥 ∈ {𝐴}) ↔ ∃!𝑦 𝐴𝐹𝑦)) |
20 | 11, 12, 19 | ralbinrald 41199 |
. . . 4
⊢ (𝐴 ∈ dom 𝐹 → (∀𝑥 ∈ dom (𝐹 ↾ {𝐴})∃!𝑦(𝑥𝐹𝑦 ∧ 𝑥 ∈ {𝐴}) ↔ ∃!𝑦 𝐴𝐹𝑦)) |
21 | 10, 20 | bitrd 268 |
. . 3
⊢ (𝐴 ∈ dom 𝐹 → (∀𝑥 ∈ dom (𝐹 ↾ {𝐴})∃!𝑦 𝑥(𝐹 ↾ {𝐴})𝑦 ↔ ∃!𝑦 𝐴𝐹𝑦)) |
22 | 21 | pm5.32i 669 |
. 2
⊢ ((𝐴 ∈ dom 𝐹 ∧ ∀𝑥 ∈ dom (𝐹 ↾ {𝐴})∃!𝑦 𝑥(𝐹 ↾ {𝐴})𝑦) ↔ (𝐴 ∈ dom 𝐹 ∧ ∃!𝑦 𝐴𝐹𝑦)) |
23 | 1, 5, 22 | 3bitri 286 |
1
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ ∃!𝑦 𝐴𝐹𝑦)) |