Proof of Theorem elpreqprlem
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢ {𝐵, 𝐶} = {𝐵, 𝐶} |
| 2 | | preq2 4734 |
. . . . . 6
⊢ (𝑥 = 𝐶 → {𝐵, 𝑥} = {𝐵, 𝐶}) |
| 3 | 2 | eqeq2d 2748 |
. . . . 5
⊢ (𝑥 = 𝐶 → ({𝐵, 𝐶} = {𝐵, 𝑥} ↔ {𝐵, 𝐶} = {𝐵, 𝐶})) |
| 4 | 3 | spcegv 3597 |
. . . 4
⊢ (𝐶 ∈ V → ({𝐵, 𝐶} = {𝐵, 𝐶} → ∃𝑥{𝐵, 𝐶} = {𝐵, 𝑥})) |
| 5 | 1, 4 | mpi 20 |
. . 3
⊢ (𝐶 ∈ V → ∃𝑥{𝐵, 𝐶} = {𝐵, 𝑥}) |
| 6 | 5 | a1d 25 |
. 2
⊢ (𝐶 ∈ V → (𝐵 ∈ 𝑉 → ∃𝑥{𝐵, 𝐶} = {𝐵, 𝑥})) |
| 7 | | dfsn2 4639 |
. . . 4
⊢ {𝐵} = {𝐵, 𝐵} |
| 8 | | preq2 4734 |
. . . . . 6
⊢ (𝑥 = 𝐵 → {𝐵, 𝑥} = {𝐵, 𝐵}) |
| 9 | 8 | eqeq2d 2748 |
. . . . 5
⊢ (𝑥 = 𝐵 → ({𝐵} = {𝐵, 𝑥} ↔ {𝐵} = {𝐵, 𝐵})) |
| 10 | 9 | spcegv 3597 |
. . . 4
⊢ (𝐵 ∈ 𝑉 → ({𝐵} = {𝐵, 𝐵} → ∃𝑥{𝐵} = {𝐵, 𝑥})) |
| 11 | 7, 10 | mpi 20 |
. . 3
⊢ (𝐵 ∈ 𝑉 → ∃𝑥{𝐵} = {𝐵, 𝑥}) |
| 12 | | prprc2 4766 |
. . . . 5
⊢ (¬
𝐶 ∈ V → {𝐵, 𝐶} = {𝐵}) |
| 13 | 12 | eqeq1d 2739 |
. . . 4
⊢ (¬
𝐶 ∈ V → ({𝐵, 𝐶} = {𝐵, 𝑥} ↔ {𝐵} = {𝐵, 𝑥})) |
| 14 | 13 | exbidv 1921 |
. . 3
⊢ (¬
𝐶 ∈ V →
(∃𝑥{𝐵, 𝐶} = {𝐵, 𝑥} ↔ ∃𝑥{𝐵} = {𝐵, 𝑥})) |
| 15 | 11, 14 | imbitrrid 246 |
. 2
⊢ (¬
𝐶 ∈ V → (𝐵 ∈ 𝑉 → ∃𝑥{𝐵, 𝐶} = {𝐵, 𝑥})) |
| 16 | 6, 15 | pm2.61i 182 |
1
⊢ (𝐵 ∈ 𝑉 → ∃𝑥{𝐵, 𝐶} = {𝐵, 𝑥}) |