Proof of Theorem abrexco
Step | Hyp | Ref
| Expression |
1 | | df-rex 2448 |
. . . . 5
⊢
(∃𝑦 ∈
{𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶 ↔ ∃𝑦(𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵} ∧ 𝑥 = 𝐶)) |
2 | | vex 2727 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
3 | | eqeq1 2171 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑦 = 𝐵)) |
4 | 3 | rexbidv 2465 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃𝑤 ∈ 𝐴 𝑦 = 𝐵)) |
5 | 2, 4 | elab 2868 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵} ↔ ∃𝑤 ∈ 𝐴 𝑦 = 𝐵) |
6 | 5 | anbi1i 454 |
. . . . . . 7
⊢ ((𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵} ∧ 𝑥 = 𝐶) ↔ (∃𝑤 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
7 | | r19.41v 2620 |
. . . . . . 7
⊢
(∃𝑤 ∈
𝐴 (𝑦 = 𝐵 ∧ 𝑥 = 𝐶) ↔ (∃𝑤 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
8 | 6, 7 | bitr4i 186 |
. . . . . 6
⊢ ((𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵} ∧ 𝑥 = 𝐶) ↔ ∃𝑤 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
9 | 8 | exbii 1592 |
. . . . 5
⊢
(∃𝑦(𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵} ∧ 𝑥 = 𝐶) ↔ ∃𝑦∃𝑤 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
10 | 1, 9 | bitri 183 |
. . . 4
⊢
(∃𝑦 ∈
{𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶 ↔ ∃𝑦∃𝑤 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
11 | | rexcom4 2747 |
. . . 4
⊢
(∃𝑤 ∈
𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 = 𝐶) ↔ ∃𝑦∃𝑤 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
12 | 10, 11 | bitr4i 186 |
. . 3
⊢
(∃𝑦 ∈
{𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶 ↔ ∃𝑤 ∈ 𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
13 | | abrexco.1 |
. . . . 5
⊢ 𝐵 ∈ V |
14 | | abrexco.2 |
. . . . . 6
⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷) |
15 | 14 | eqeq2d 2176 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝑥 = 𝐶 ↔ 𝑥 = 𝐷)) |
16 | 13, 15 | ceqsexv 2763 |
. . . 4
⊢
(∃𝑦(𝑦 = 𝐵 ∧ 𝑥 = 𝐶) ↔ 𝑥 = 𝐷) |
17 | 16 | rexbii 2471 |
. . 3
⊢
(∃𝑤 ∈
𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 = 𝐶) ↔ ∃𝑤 ∈ 𝐴 𝑥 = 𝐷) |
18 | 12, 17 | bitri 183 |
. 2
⊢
(∃𝑦 ∈
{𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶 ↔ ∃𝑤 ∈ 𝐴 𝑥 = 𝐷) |
19 | 18 | abbii 2280 |
1
⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶} = {𝑥 ∣ ∃𝑤 ∈ 𝐴 𝑥 = 𝐷} |