Step | Hyp | Ref
| Expression |
1 | | 19.42v 2052 |
. . 3
⊢
(∃𝑥(∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) ↔ (∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑)))) |
2 | | bimsc1 875 |
. . . . 5
⊢ (((𝜑 → 𝑦 ∈ 𝑧) ∧ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) → (𝑦 ∈ 𝑥 ↔ 𝜑)) |
3 | 2 | alanimi 1915 |
. . . 4
⊢
((∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) → ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) |
4 | 3 | eximi 1933 |
. . 3
⊢
(∃𝑥(∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) → ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) |
5 | 1, 4 | sylbir 227 |
. 2
⊢
((∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) → ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) |
6 | | bm1.3ii.1 |
. . . . 5
⊢
∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥) |
7 | | elequ2 2178 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)) |
8 | 7 | imbi2d 332 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝜑 → 𝑦 ∈ 𝑥) ↔ (𝜑 → 𝑦 ∈ 𝑧))) |
9 | 8 | albidv 2019 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (∀𝑦(𝜑 → 𝑦 ∈ 𝑥) ↔ ∀𝑦(𝜑 → 𝑦 ∈ 𝑧))) |
10 | 9 | cbvexvw 2144 |
. . . . 5
⊢
(∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥) ↔ ∃𝑧∀𝑦(𝜑 → 𝑦 ∈ 𝑧)) |
11 | 6, 10 | mpbi 222 |
. . . 4
⊢
∃𝑧∀𝑦(𝜑 → 𝑦 ∈ 𝑧) |
12 | | ax-sep 5007 |
. . . 4
⊢
∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑)) |
13 | 11, 12 | pm3.2i 464 |
. . 3
⊢
(∃𝑧∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) |
14 | 13 | exan 1961 |
. 2
⊢
∃𝑧(∀𝑦(𝜑 → 𝑦 ∈ 𝑧) ∧ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝑧 ∧ 𝜑))) |
15 | 5, 14 | exlimiiv 2030 |
1
⊢
∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) |