Step | Hyp | Ref
| Expression |
1 | | ax-ext 2711 |
. . . . . 6
⊢
(∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → 𝑥 = 𝑧) |
2 | 1 | alimi 1818 |
. . . . 5
⊢
(∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥 𝑥 = 𝑧) |
3 | | ax-11 2158 |
. . . . . . 7
⊢
(∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧)) |
4 | | ax9 2124 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧)) |
5 | | biimpr 219 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)) |
6 | 5 | alimi 1818 |
. . . . . . . . . 10
⊢
(∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)) |
7 | | stdpc5v 1945 |
. . . . . . . . . 10
⊢
(∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥)) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢
(∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥)) |
9 | 4, 8 | syl9 77 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))) |
10 | 9 | alimdv 1923 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))) |
11 | 3, 10 | syl5 34 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))) |
12 | 11 | sps 2182 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))) |
13 | 2, 12 | mpcom 38 |
. . . 4
⊢
(∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)) |
14 | 13 | axc4i 2320 |
. . 3
⊢
(∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)) |
15 | | nfa1 2152 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 𝑤 ∈ 𝑥 |
16 | 15 | 19.23 2208 |
. . . . . . 7
⊢
(∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) ↔ (∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)) |
17 | | 19.8a 2178 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑧 → ∃𝑧 𝑤 ∈ 𝑧) |
18 | | elequ2 2125 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥)) |
19 | 18 | cbvexvw 2044 |
. . . . . . . . 9
⊢
(∃𝑧 𝑤 ∈ 𝑧 ↔ ∃𝑥 𝑤 ∈ 𝑥) |
20 | 17, 19 | sylib 217 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑧 → ∃𝑥 𝑤 ∈ 𝑥) |
21 | 4 | cbvalivw 2014 |
. . . . . . . 8
⊢
(∀𝑥 𝑤 ∈ 𝑥 → ∀𝑧 𝑤 ∈ 𝑧) |
22 | 20, 21 | imim12i 62 |
. . . . . . 7
⊢
((∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧)) |
23 | 16, 22 | sylbi 216 |
. . . . . 6
⊢
(∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧)) |
24 | 23 | alimi 1818 |
. . . . 5
⊢
(∀𝑤∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧)) |
25 | 24 | alcoms 2159 |
. . . 4
⊢
(∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧)) |
26 | 25 | alrimiv 1934 |
. . 3
⊢
(∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧)) |
27 | | nfa1 2152 |
. . . . . . . 8
⊢
Ⅎ𝑧∀𝑧 𝑤 ∈ 𝑧 |
28 | 27 | 19.23 2208 |
. . . . . . 7
⊢
(∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) ↔ (∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧)) |
29 | | ax9 2124 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)) |
30 | 29 | spimvw 2003 |
. . . . . . . . 9
⊢
(∀𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) |
31 | 17, 30 | imim12i 62 |
. . . . . . . 8
⊢
((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)) |
32 | | 19.8a 2178 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝑥 → ∃𝑥 𝑤 ∈ 𝑥) |
33 | | elequ2 2125 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧)) |
34 | 33 | cbvexvw 2044 |
. . . . . . . . . 10
⊢
(∃𝑥 𝑤 ∈ 𝑥 ↔ ∃𝑧 𝑤 ∈ 𝑧) |
35 | 32, 34 | sylib 217 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑥 → ∃𝑧 𝑤 ∈ 𝑧) |
36 | | sp 2180 |
. . . . . . . . 9
⊢
(∀𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑧) |
37 | 35, 36 | imim12i 62 |
. . . . . . . 8
⊢
((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧)) |
38 | 31, 37 | impbid 211 |
. . . . . . 7
⊢
((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥)) |
39 | 28, 38 | sylbi 216 |
. . . . . 6
⊢
(∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥)) |
40 | 39 | alimi 1818 |
. . . . 5
⊢
(∀𝑤∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥)) |
41 | 40 | alcoms 2159 |
. . . 4
⊢
(∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥)) |
42 | 41 | axc4i 2320 |
. . 3
⊢
(∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥)) |
43 | 14, 26, 42 | 3syl 18 |
. 2
⊢
(∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥)) |
44 | | axextb 2714 |
. . 3
⊢ (𝑥 = 𝑧 ↔ ∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧)) |
45 | 44 | albii 1826 |
. 2
⊢
(∀𝑥 𝑥 = 𝑧 ↔ ∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧)) |
46 | | axextb 2714 |
. . 3
⊢ (𝑧 = 𝑥 ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥)) |
47 | 46 | albii 1826 |
. 2
⊢
(∀𝑧 𝑧 = 𝑥 ↔ ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥)) |
48 | 43, 45, 47 | 3imtr4i 292 |
1
⊢
(∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥) |