Step | Hyp | Ref
| Expression |
1 | | bdbm1.3ii.1 |
. . . . 5
⊢
∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥) |
2 | | elequ2 2146 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)) |
3 | 2 | imbi2d 229 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝜑 → 𝑦 ∈ 𝑥) ↔ (𝜑 → 𝑦 ∈ 𝑧))) |
4 | 3 | albidv 1817 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (∀𝑦(𝜑 → 𝑦 ∈ 𝑥) ↔ ∀𝑦(𝜑 → 𝑦 ∈ 𝑧))) |
5 | 4 | cbvexv 1911 |
. . . . 5
⊢
(∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥) ↔ ∃𝑧∀𝑦(𝜑 → 𝑦 ∈ 𝑧)) |
6 | 1, 5 | mpbi 144 |
. . . 4
⊢
∃𝑧∀𝑦(𝜑 → 𝑦 ∈ 𝑧) |
7 | | bdbm1.3ii.bd |
. . . . 5
⊢
BOUNDED 𝜑 |
8 | 7 | bdsep1 13885 |
. . . 4
⊢
∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑)) |
9 | 6, 8 | pm3.2i 270 |
. . 3
⊢
(∃𝑧∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) |
10 | 9 | exan 1686 |
. 2
⊢
∃𝑧(∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) |
11 | | 19.42v 1899 |
. . . 4
⊢
(∃𝑥(∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) ↔ (∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑)))) |
12 | | bimsc1 958 |
. . . . . 6
⊢ (((𝜑 → 𝑦 ∈ 𝑧) ∧ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) → (𝑦 ∈ 𝑥 ↔ 𝜑)) |
13 | 12 | alanimi 1452 |
. . . . 5
⊢
((∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) → ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) |
14 | 13 | eximi 1593 |
. . . 4
⊢
(∃𝑥(∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) → ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) |
15 | 11, 14 | sylbir 134 |
. . 3
⊢
((∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) → ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) |
16 | 15 | exlimiv 1591 |
. 2
⊢
(∃𝑧(∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) → ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) |
17 | 10, 16 | ax-mp 5 |
1
⊢
∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) |