Step | Hyp | Ref
| Expression |
1 | | nfnae 2434 |
. . . . . . . 8
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
2 | | nfnae 2434 |
. . . . . . . 8
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑧 |
3 | 1, 2 | nfan 1902 |
. . . . . . 7
⊢
Ⅎ𝑥(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
4 | | nfcvf 2936 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
5 | 4 | adantr 481 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦) |
6 | 5 | nfcrd 2896 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤 ∈ 𝑦) |
7 | | nfcvf 2936 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝑧) |
8 | 7 | adantl 482 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧) |
9 | 8 | nfcrd 2896 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤 ∈ 𝑧) |
10 | 6, 9 | nfbid 1905 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑤 ∈ 𝑦 ↔ 𝑤 ∈ 𝑧)) |
11 | | elequ1 2113 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) |
12 | | elequ1 2113 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)) |
13 | 11, 12 | bibi12d 346 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑦 ↔ 𝑤 ∈ 𝑧) ↔ (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧))) |
14 | 13 | a1i 11 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((𝑤 ∈ 𝑦 ↔ 𝑤 ∈ 𝑧) ↔ (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧)))) |
15 | 3, 10, 14 | cbvald 2407 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑤(𝑤 ∈ 𝑦 ↔ 𝑤 ∈ 𝑧) ↔ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧))) |
16 | | axextg 2711 |
. . . . . 6
⊢
(∀𝑤(𝑤 ∈ 𝑦 ↔ 𝑤 ∈ 𝑧) → 𝑦 = 𝑧) |
17 | 15, 16 | syl6bir 253 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)) |
18 | | 19.8a 2174 |
. . . . 5
⊢ (𝑦 = 𝑧 → ∃𝑥 𝑦 = 𝑧) |
19 | 17, 18 | syl6 35 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → ∃𝑥 𝑦 = 𝑧)) |
20 | 19 | ex 413 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → ∃𝑥 𝑦 = 𝑧))) |
21 | | ax6e 2383 |
. . . . 5
⊢
∃𝑥 𝑥 = 𝑧 |
22 | | ax7 2019 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) |
23 | 22 | aleximi 1834 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥 𝑥 = 𝑧 → ∃𝑥 𝑦 = 𝑧)) |
24 | 21, 23 | mpi 20 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → ∃𝑥 𝑦 = 𝑧) |
25 | 24 | a1d 25 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → ∃𝑥 𝑦 = 𝑧)) |
26 | | ax6e 2383 |
. . . . 5
⊢
∃𝑥 𝑥 = 𝑦 |
27 | | ax7 2019 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 → 𝑧 = 𝑦)) |
28 | | equcomi 2020 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → 𝑦 = 𝑧) |
29 | 27, 28 | syl6 35 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 → 𝑦 = 𝑧)) |
30 | 29 | aleximi 1834 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑧 → (∃𝑥 𝑥 = 𝑦 → ∃𝑥 𝑦 = 𝑧)) |
31 | 26, 30 | mpi 20 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑧 → ∃𝑥 𝑦 = 𝑧) |
32 | 31 | a1d 25 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → ∃𝑥 𝑦 = 𝑧)) |
33 | 20, 25, 32 | pm2.61ii 183 |
. 2
⊢
(∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → ∃𝑥 𝑦 = 𝑧) |
34 | 33 | 19.35ri 1882 |
1
⊢
∃𝑥((𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧) |