| Step | Hyp | Ref
| Expression |
| 1 | | preq2 4734 |
. . . . . 6
⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵}) |
| 2 | 1 | eleq1d 2826 |
. . . . 5
⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V)) |
| 3 | | zfpair2 5433 |
. . . . 5
⊢ {𝑥, 𝑦} ∈ V |
| 4 | 2, 3 | vtoclg 3554 |
. . . 4
⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V) |
| 5 | | preq1 4733 |
. . . . 5
⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵}) |
| 6 | 5 | eleq1d 2826 |
. . . 4
⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V)) |
| 7 | 4, 6 | imbitrid 244 |
. . 3
⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V)) |
| 8 | 7 | vtocleg 3553 |
. 2
⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V)) |
| 9 | | prprc1 4765 |
. . 3
⊢ (¬
𝐴 ∈ V → {𝐴, 𝐵} = {𝐵}) |
| 10 | | snex 5436 |
. . 3
⊢ {𝐵} ∈ V |
| 11 | 9, 10 | eqeltrdi 2849 |
. 2
⊢ (¬
𝐴 ∈ V → {𝐴, 𝐵} ∈ V) |
| 12 | | prprc2 4766 |
. . 3
⊢ (¬
𝐵 ∈ V → {𝐴, 𝐵} = {𝐴}) |
| 13 | | snex 5436 |
. . 3
⊢ {𝐴} ∈ V |
| 14 | 12, 13 | eqeltrdi 2849 |
. 2
⊢ (¬
𝐵 ∈ V → {𝐴, 𝐵} ∈ V) |
| 15 | 8, 11, 14 | pm2.61nii 184 |
1
⊢ {𝐴, 𝐵} ∈ V |