Proof of Theorem axrep4
Step | Hyp | Ref
| Expression |
1 | | axrep3 5218 |
. . 3
⊢
∃𝑥(∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∀𝑦(𝑦 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑))) |
2 | 1 | 19.35i 1885 |
. 2
⊢
(∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑))) |
3 | | nfv 1921 |
. . . . 5
⊢
Ⅎ𝑧 𝑦 ∈ 𝑥 |
4 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑧 𝑥 ∈ 𝑤 |
5 | | nfa1 2152 |
. . . . . . 7
⊢
Ⅎ𝑧∀𝑧𝜑 |
6 | 4, 5 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑧(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑) |
7 | 6 | nfex 2322 |
. . . . 5
⊢
Ⅎ𝑧∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑) |
8 | 3, 7 | nfbi 1910 |
. . . 4
⊢
Ⅎ𝑧(𝑦 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑)) |
9 | 8 | nfal 2321 |
. . 3
⊢
Ⅎ𝑧∀𝑦(𝑦 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑)) |
10 | | nfv 1921 |
. . . . 5
⊢
Ⅎ𝑥 𝑦 ∈ 𝑧 |
11 | | nfe1 2151 |
. . . . 5
⊢
Ⅎ𝑥∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑) |
12 | 10, 11 | nfbi 1910 |
. . . 4
⊢
Ⅎ𝑥(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)) |
13 | 12 | nfal 2321 |
. . 3
⊢
Ⅎ𝑥∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)) |
14 | | elequ2 2125 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)) |
15 | | axrep4.1 |
. . . . . . . . 9
⊢
Ⅎ𝑧𝜑 |
16 | 15 | 19.3 2199 |
. . . . . . . 8
⊢
(∀𝑧𝜑 ↔ 𝜑) |
17 | 16 | anbi2i 623 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑) ↔ (𝑥 ∈ 𝑤 ∧ 𝜑)) |
18 | 17 | exbii 1854 |
. . . . . 6
⊢
(∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)) |
19 | 18 | a1i 11 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) |
20 | 14, 19 | bibi12d 346 |
. . . 4
⊢ (𝑥 = 𝑧 → ((𝑦 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑)) ↔ (𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))) |
21 | 20 | albidv 1927 |
. . 3
⊢ (𝑥 = 𝑧 → (∀𝑦(𝑦 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑)) ↔ ∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))) |
22 | 9, 13, 21 | cbvexv1 2343 |
. 2
⊢
(∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑)) ↔ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) |
23 | 2, 22 | sylib 217 |
1
⊢
(∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) |