Step | Hyp | Ref
| Expression |
1 | | ax-ac 9959 |
. 2
⊢
∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) |
2 | | equequ2 2038 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑤 → (𝑢 = 𝑣 ↔ 𝑢 = 𝑤)) |
3 | 2 | bibi2d 346 |
. . . . . . . . 9
⊢ (𝑣 = 𝑤 → ((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ (∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑤))) |
4 | | elequ2 2129 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑤 → (𝑧 ∈ 𝑡 ↔ 𝑧 ∈ 𝑤)) |
5 | 4 | anbi2d 632 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑤 → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ↔ (𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) |
6 | | elequ2 2129 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑤 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑤)) |
7 | | elequ1 2121 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑤 → (𝑡 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥)) |
8 | 6, 7 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑤 → ((𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥) ↔ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))) |
9 | 5, 8 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑤 → (((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))) |
10 | 9 | cbvexvw 2049 |
. . . . . . . . . 10
⊢
(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ ∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))) |
11 | 10 | bibi1i 342 |
. . . . . . . . 9
⊢
((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤)) |
12 | 3, 11 | bitrdi 290 |
. . . . . . . 8
⊢ (𝑣 = 𝑤 → ((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤))) |
13 | 12 | albidv 1927 |
. . . . . . 7
⊢ (𝑣 = 𝑤 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∀𝑢(∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤))) |
14 | | elequ1 2121 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑦 → (𝑢 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧)) |
15 | 14 | anbi1d 633 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑦 → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) |
16 | | elequ1 2121 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑦 → (𝑢 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤)) |
17 | 16 | anbi1d 633 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑦 → ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ↔ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))) |
18 | 15, 17 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑦 → (((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))) |
19 | 18 | exbidv 1928 |
. . . . . . . . 9
⊢ (𝑢 = 𝑦 → (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))) |
20 | | equequ1 2037 |
. . . . . . . . 9
⊢ (𝑢 = 𝑦 → (𝑢 = 𝑤 ↔ 𝑦 = 𝑤)) |
21 | 19, 20 | bibi12d 349 |
. . . . . . . 8
⊢ (𝑢 = 𝑦 → ((∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ (∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
22 | 21 | cbvalvw 2048 |
. . . . . . 7
⊢
(∀𝑢(∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) |
23 | 13, 22 | bitrdi 290 |
. . . . . 6
⊢ (𝑣 = 𝑤 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
24 | 23 | cbvexvw 2049 |
. . . . 5
⊢
(∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) |
25 | 24 | imbi2i 339 |
. . . 4
⊢ (((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
26 | 25 | 2albii 1827 |
. . 3
⊢
(∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
27 | 26 | exbii 1854 |
. 2
⊢
(∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
28 | 1, 27 | mpbi 233 |
1
⊢
∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) |