Step | Hyp | Ref
| Expression |
1 | | nfnae 2433 |
. . . 4
⊢
Ⅎ𝑧 ¬
∀𝑧 𝑧 = 𝑥 |
2 | | nfnae 2433 |
. . . 4
⊢
Ⅎ𝑧 ¬
∀𝑧 𝑧 = 𝑦 |
3 | 1, 2 | nfan 1905 |
. . 3
⊢
Ⅎ𝑧(¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) |
4 | | nfcvf 2928 |
. . . . . 6
⊢ (¬
∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧𝑥) |
5 | 4 | adantr 484 |
. . . . 5
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧𝑥) |
6 | 5 | nfcrd 2888 |
. . . 4
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑤 ∈ 𝑥) |
7 | | nfcvf 2928 |
. . . . . 6
⊢ (¬
∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧𝑦) |
8 | 7 | adantl 485 |
. . . . 5
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧𝑦) |
9 | 8 | nfcrd 2888 |
. . . 4
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑤 ∈ 𝑦) |
10 | 6, 9 | nfbid 1908 |
. . 3
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)) |
11 | | elequ1 2120 |
. . . . 5
⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
12 | | elequ1 2120 |
. . . . 5
⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦)) |
13 | 11, 12 | bibi12d 349 |
. . . 4
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦) ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))) |
14 | 13 | a1i 11 |
. . 3
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦) ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)))) |
15 | 3, 10, 14 | cbvald 2406 |
. 2
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))) |
16 | | axextg 2712 |
. 2
⊢
(∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦) |
17 | 15, 16 | syl6bir 257 |
1
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)) |