Proof of Theorem equvel
Step | Hyp | Ref
| Expression |
1 | | albi 1810 |
. 2
⊢
(∀𝑧(𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → (∀𝑧 𝑧 = 𝑥 ↔ ∀𝑧 𝑧 = 𝑦)) |
2 | | ax6e 2392 |
. . . 4
⊢
∃𝑧 𝑧 = 𝑦 |
3 | | biimpr 221 |
. . . . . 6
⊢ ((𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → (𝑧 = 𝑦 → 𝑧 = 𝑥)) |
4 | | ax7 2014 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝑧 = 𝑦 → 𝑥 = 𝑦)) |
5 | 3, 4 | syli 39 |
. . . . 5
⊢ ((𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → (𝑧 = 𝑦 → 𝑥 = 𝑦)) |
6 | 5 | com12 32 |
. . . 4
⊢ (𝑧 = 𝑦 → ((𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → 𝑥 = 𝑦)) |
7 | 2, 6 | eximii 1828 |
. . 3
⊢
∃𝑧((𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → 𝑥 = 𝑦) |
8 | 7 | 19.35i 1870 |
. 2
⊢
(∀𝑧(𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → ∃𝑧 𝑥 = 𝑦) |
9 | 4 | spsd 2176 |
. . . . 5
⊢ (𝑧 = 𝑥 → (∀𝑧 𝑧 = 𝑦 → 𝑥 = 𝑦)) |
10 | 9 | sps 2174 |
. . . 4
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑧 𝑧 = 𝑦 → 𝑥 = 𝑦)) |
11 | 10 | a1dd 50 |
. . 3
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑧 𝑧 = 𝑦 → (∃𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦))) |
12 | | nfeqf 2390 |
. . . . 5
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑥 = 𝑦) |
13 | 12 | 19.9d 2193 |
. . . 4
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∃𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
14 | 13 | ex 413 |
. . 3
⊢ (¬
∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (∃𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦))) |
15 | 11, 14 | bija 382 |
. 2
⊢
((∀𝑧 𝑧 = 𝑥 ↔ ∀𝑧 𝑧 = 𝑦) → (∃𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
16 | 1, 8, 15 | sylc 65 |
1
⊢
(∀𝑧(𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → 𝑥 = 𝑦) |