Step | Hyp | Ref
| Expression |
1 | | nfnae 2434 |
. . . 4
⊢
Ⅎ𝑧 ¬
∀𝑧 𝑧 = 𝑥 |
2 | | nfnae 2434 |
. . . 4
⊢
Ⅎ𝑧 ¬
∀𝑧 𝑧 = 𝑦 |
3 | 1, 2 | nfan 1902 |
. . 3
⊢
Ⅎ𝑧(¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) |
4 | | nfcvf 2936 |
. . . . . 6
⊢ (¬
∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧𝑥) |
5 | 4 | adantr 481 |
. . . . 5
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧𝑥) |
6 | 5 | nfcrd 2896 |
. . . 4
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑤 ∈ 𝑥) |
7 | | nfcvf 2936 |
. . . . . 6
⊢ (¬
∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧𝑦) |
8 | 7 | adantl 482 |
. . . . 5
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧𝑦) |
9 | 8 | nfcrd 2896 |
. . . 4
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑤 ∈ 𝑦) |
10 | 6, 9 | nfbid 1905 |
. . 3
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)) |
11 | | elequ1 2113 |
. . . . 5
⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
12 | | elequ1 2113 |
. . . . 5
⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦)) |
13 | 11, 12 | bibi12d 346 |
. . . 4
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦) ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))) |
14 | 13 | a1i 11 |
. . 3
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦) ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)))) |
15 | 3, 10, 14 | cbvald 2407 |
. 2
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))) |
16 | | axextg 2711 |
. 2
⊢
(∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦) |
17 | 15, 16 | syl6bir 253 |
1
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)) |