| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elex 3501 | . 2
⊢ (𝐴 ∈ dom 𝐵 → 𝐴 ∈ V) | 
| 2 |  | snprc 4717 | . . . 4
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) | 
| 3 |  | reseq2 5992 | . . . . 5
⊢ ({𝐴} = ∅ → (𝐵 ↾ {𝐴}) = (𝐵 ↾ ∅)) | 
| 4 |  | res0 6001 | . . . . 5
⊢ (𝐵 ↾ ∅) =
∅ | 
| 5 | 3, 4 | eqtrdi 2793 | . . . 4
⊢ ({𝐴} = ∅ → (𝐵 ↾ {𝐴}) = ∅) | 
| 6 | 2, 5 | sylbi 217 | . . 3
⊢ (¬
𝐴 ∈ V → (𝐵 ↾ {𝐴}) = ∅) | 
| 7 | 6 | necon1ai 2968 | . 2
⊢ ((𝐵 ↾ {𝐴}) ≠ ∅ → 𝐴 ∈ V) | 
| 8 |  | eleq1 2829 | . . 3
⊢ (𝑥 = 𝐴 → (𝑥 ∈ dom 𝐵 ↔ 𝐴 ∈ dom 𝐵)) | 
| 9 |  | sneq 4636 | . . . . 5
⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴}) | 
| 10 | 9 | reseq2d 5997 | . . . 4
⊢ (𝑥 = 𝐴 → (𝐵 ↾ {𝑥}) = (𝐵 ↾ {𝐴})) | 
| 11 | 10 | neeq1d 3000 | . . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ↾ {𝑥}) ≠ ∅ ↔ (𝐵 ↾ {𝐴}) ≠ ∅)) | 
| 12 |  | dfclel 2817 | . . . . 5
⊢
(〈𝑥, 𝑦〉 ∈ 𝐵 ↔ ∃𝑝(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) | 
| 13 | 12 | exbii 1848 | . . . 4
⊢
(∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵 ↔ ∃𝑦∃𝑝(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) | 
| 14 |  | vex 3484 | . . . . 5
⊢ 𝑥 ∈ V | 
| 15 | 14 | eldm2 5912 | . . . 4
⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵) | 
| 16 |  | n0 4353 | . . . . 5
⊢ ((𝐵 ↾ {𝑥}) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝐵 ↾ {𝑥})) | 
| 17 |  | elres 6038 | . . . . . . 7
⊢ (𝑝 ∈ (𝐵 ↾ {𝑥}) ↔ ∃𝑧 ∈ {𝑥}∃𝑦(𝑝 = 〈𝑧, 𝑦〉 ∧ 〈𝑧, 𝑦〉 ∈ 𝐵)) | 
| 18 |  | eleq1 2829 | . . . . . . . . . . 11
⊢ (𝑝 = 〈𝑧, 𝑦〉 → (𝑝 ∈ 𝐵 ↔ 〈𝑧, 𝑦〉 ∈ 𝐵)) | 
| 19 | 18 | pm5.32i 574 | . . . . . . . . . 10
⊢ ((𝑝 = 〈𝑧, 𝑦〉 ∧ 𝑝 ∈ 𝐵) ↔ (𝑝 = 〈𝑧, 𝑦〉 ∧ 〈𝑧, 𝑦〉 ∈ 𝐵)) | 
| 20 |  | opeq1 4873 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → 〈𝑧, 𝑦〉 = 〈𝑥, 𝑦〉) | 
| 21 | 20 | eqeq2d 2748 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (𝑝 = 〈𝑧, 𝑦〉 ↔ 𝑝 = 〈𝑥, 𝑦〉)) | 
| 22 | 21 | anbi1d 631 | . . . . . . . . . 10
⊢ (𝑧 = 𝑥 → ((𝑝 = 〈𝑧, 𝑦〉 ∧ 𝑝 ∈ 𝐵) ↔ (𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵))) | 
| 23 | 19, 22 | bitr3id 285 | . . . . . . . . 9
⊢ (𝑧 = 𝑥 → ((𝑝 = 〈𝑧, 𝑦〉 ∧ 〈𝑧, 𝑦〉 ∈ 𝐵) ↔ (𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵))) | 
| 24 | 23 | exbidv 1921 | . . . . . . . 8
⊢ (𝑧 = 𝑥 → (∃𝑦(𝑝 = 〈𝑧, 𝑦〉 ∧ 〈𝑧, 𝑦〉 ∈ 𝐵) ↔ ∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵))) | 
| 25 | 14, 24 | rexsn 4682 | . . . . . . 7
⊢
(∃𝑧 ∈
{𝑥}∃𝑦(𝑝 = 〈𝑧, 𝑦〉 ∧ 〈𝑧, 𝑦〉 ∈ 𝐵) ↔ ∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) | 
| 26 | 17, 25 | bitri 275 | . . . . . 6
⊢ (𝑝 ∈ (𝐵 ↾ {𝑥}) ↔ ∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) | 
| 27 | 26 | exbii 1848 | . . . . 5
⊢
(∃𝑝 𝑝 ∈ (𝐵 ↾ {𝑥}) ↔ ∃𝑝∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) | 
| 28 |  | excom 2162 | . . . . 5
⊢
(∃𝑝∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵) ↔ ∃𝑦∃𝑝(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) | 
| 29 | 16, 27, 28 | 3bitri 297 | . . . 4
⊢ ((𝐵 ↾ {𝑥}) ≠ ∅ ↔ ∃𝑦∃𝑝(𝑝 = 〈𝑥, 𝑦〉 ∧ 𝑝 ∈ 𝐵)) | 
| 30 | 13, 15, 29 | 3bitr4i 303 | . . 3
⊢ (𝑥 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝑥}) ≠ ∅) | 
| 31 | 8, 11, 30 | vtoclbg 3557 | . 2
⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅)) | 
| 32 | 1, 7, 31 | pm5.21nii 378 | 1
⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅) |