Step | Hyp | Ref
| Expression |
1 | | elex 3438 |
. 2
⊢ (𝐴 ∈ dom 𝐵 → 𝐴 ∈ V) |
2 | | snprc 4647 |
. . . 4
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) |
3 | | reseq2 5860 |
. . . . 5
⊢ ({𝐴} = ∅ → (𝐵 ↾ {𝐴}) = (𝐵 ↾ ∅)) |
4 | | res0 5869 |
. . . . 5
⊢ (𝐵 ↾ ∅) =
∅ |
5 | 3, 4 | eqtrdi 2795 |
. . . 4
⊢ ({𝐴} = ∅ → (𝐵 ↾ {𝐴}) = ∅) |
6 | 2, 5 | sylbi 220 |
. . 3
⊢ (¬
𝐴 ∈ V → (𝐵 ↾ {𝐴}) = ∅) |
7 | 6 | necon1ai 2969 |
. 2
⊢ ((𝐵 ↾ {𝐴}) ≠ ∅ → 𝐴 ∈ V) |
8 | | eleq1 2826 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑥 ∈ dom 𝐵 ↔ 𝐴 ∈ dom 𝐵)) |
9 | | sneq 4565 |
. . . . 5
⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴}) |
10 | 9 | reseq2d 5865 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝐵 ↾ {𝑥}) = (𝐵 ↾ {𝐴})) |
11 | 10 | neeq1d 3001 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ↾ {𝑥}) ≠ ∅ ↔ (𝐵 ↾ {𝐴}) ≠ ∅)) |
12 | | dfclel 2818 |
. . . . 5
⊢
(〈𝑥, 𝑦〉 ∈ 𝐵 ↔ ∃𝑝(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) |
13 | 12 | exbii 1855 |
. . . 4
⊢
(∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵 ↔ ∃𝑦∃𝑝(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) |
14 | | vex 3424 |
. . . . 5
⊢ 𝑥 ∈ V |
15 | 14 | eldm2 5784 |
. . . 4
⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵) |
16 | | n0 4275 |
. . . . 5
⊢ ((𝐵 ↾ {𝑥}) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝐵 ↾ {𝑥})) |
17 | | elres 5904 |
. . . . . . 7
⊢ (𝑝 ∈ (𝐵 ↾ {𝑥}) ↔ ∃𝑧 ∈ {𝑥}∃𝑦(𝑝 = 〈𝑧, 𝑦〉 ∧ 〈𝑧, 𝑦〉 ∈ 𝐵)) |
18 | | eleq1 2826 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑧, 𝑦〉 → (𝑝 ∈ 𝐵 ↔ 〈𝑧, 𝑦〉 ∈ 𝐵)) |
19 | 18 | pm5.32i 578 |
. . . . . . . . . 10
⊢ ((𝑝 = 〈𝑧, 𝑦〉 ∧ 𝑝 ∈ 𝐵) ↔ (𝑝 = 〈𝑧, 𝑦〉 ∧ 〈𝑧, 𝑦〉 ∈ 𝐵)) |
20 | | opeq1 4798 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → 〈𝑧, 𝑦〉 = 〈𝑥, 𝑦〉) |
21 | 20 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (𝑝 = 〈𝑧, 𝑦〉 ↔ 𝑝 = 〈𝑥, 𝑦〉)) |
22 | 21 | anbi1d 633 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → ((𝑝 = 〈𝑧, 𝑦〉 ∧ 𝑝 ∈ 𝐵) ↔ (𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵))) |
23 | 19, 22 | bitr3id 288 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → ((𝑝 = 〈𝑧, 𝑦〉 ∧ 〈𝑧, 𝑦〉 ∈ 𝐵) ↔ (𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵))) |
24 | 23 | exbidv 1929 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (∃𝑦(𝑝 = 〈𝑧, 𝑦〉 ∧ 〈𝑧, 𝑦〉 ∈ 𝐵) ↔ ∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵))) |
25 | 14, 24 | rexsn 4612 |
. . . . . . 7
⊢
(∃𝑧 ∈
{𝑥}∃𝑦(𝑝 = 〈𝑧, 𝑦〉 ∧ 〈𝑧, 𝑦〉 ∈ 𝐵) ↔ ∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) |
26 | 17, 25 | bitri 278 |
. . . . . 6
⊢ (𝑝 ∈ (𝐵 ↾ {𝑥}) ↔ ∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) |
27 | 26 | exbii 1855 |
. . . . 5
⊢
(∃𝑝 𝑝 ∈ (𝐵 ↾ {𝑥}) ↔ ∃𝑝∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) |
28 | | excom 2167 |
. . . . 5
⊢
(∃𝑝∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵) ↔ ∃𝑦∃𝑝(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) |
29 | 16, 27, 28 | 3bitri 300 |
. . . 4
⊢ ((𝐵 ↾ {𝑥}) ≠ ∅ ↔ ∃𝑦∃𝑝(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) |
30 | 13, 15, 29 | 3bitr4i 306 |
. . 3
⊢ (𝑥 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝑥}) ≠ ∅) |
31 | 8, 11, 30 | vtoclbg 3495 |
. 2
⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅)) |
32 | 1, 7, 31 | pm5.21nii 383 |
1
⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅) |