Proof of Theorem abrexco
| Step | Hyp | Ref
| Expression |
| 1 | | df-rex 3071 |
. . . . 5
⊢
(∃𝑦 ∈
{𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶 ↔ ∃𝑦(𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵} ∧ 𝑥 = 𝐶)) |
| 2 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
| 3 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑦 = 𝐵)) |
| 4 | 3 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃𝑤 ∈ 𝐴 𝑦 = 𝐵)) |
| 5 | 2, 4 | elab 3679 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵} ↔ ∃𝑤 ∈ 𝐴 𝑦 = 𝐵) |
| 6 | 5 | anbi1i 624 |
. . . . . . 7
⊢ ((𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵} ∧ 𝑥 = 𝐶) ↔ (∃𝑤 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
| 7 | | r19.41v 3189 |
. . . . . . 7
⊢
(∃𝑤 ∈
𝐴 (𝑦 = 𝐵 ∧ 𝑥 = 𝐶) ↔ (∃𝑤 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
| 8 | 6, 7 | bitr4i 278 |
. . . . . 6
⊢ ((𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵} ∧ 𝑥 = 𝐶) ↔ ∃𝑤 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
| 9 | 8 | exbii 1848 |
. . . . 5
⊢
(∃𝑦(𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵} ∧ 𝑥 = 𝐶) ↔ ∃𝑦∃𝑤 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
| 10 | 1, 9 | bitri 275 |
. . . 4
⊢
(∃𝑦 ∈
{𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶 ↔ ∃𝑦∃𝑤 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
| 11 | | rexcom4 3288 |
. . . 4
⊢
(∃𝑤 ∈
𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 = 𝐶) ↔ ∃𝑦∃𝑤 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
| 12 | 10, 11 | bitr4i 278 |
. . 3
⊢
(∃𝑦 ∈
{𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶 ↔ ∃𝑤 ∈ 𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 = 𝐶)) |
| 13 | | abrexco.1 |
. . . . 5
⊢ 𝐵 ∈ V |
| 14 | | abrexco.2 |
. . . . . 6
⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷) |
| 15 | 14 | eqeq2d 2748 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝑥 = 𝐶 ↔ 𝑥 = 𝐷)) |
| 16 | 13, 15 | ceqsexv 3532 |
. . . 4
⊢
(∃𝑦(𝑦 = 𝐵 ∧ 𝑥 = 𝐶) ↔ 𝑥 = 𝐷) |
| 17 | 16 | rexbii 3094 |
. . 3
⊢
(∃𝑤 ∈
𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 = 𝐶) ↔ ∃𝑤 ∈ 𝐴 𝑥 = 𝐷) |
| 18 | 12, 17 | bitri 275 |
. 2
⊢
(∃𝑦 ∈
{𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶 ↔ ∃𝑤 ∈ 𝐴 𝑥 = 𝐷) |
| 19 | 18 | abbii 2809 |
1
⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶} = {𝑥 ∣ ∃𝑤 ∈ 𝐴 𝑥 = 𝐷} |