Proof of Theorem equvel
Step | Hyp | Ref
| Expression |
1 | | albi 1736 |
. 2
⊢
(∀𝑧(𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → (∀𝑧 𝑧 = 𝑥 ↔ ∀𝑧 𝑧 = 𝑦)) |
2 | | ax6e 2238 |
. . . 4
⊢
∃𝑧 𝑧 = 𝑦 |
3 | | biimpr 209 |
. . . . . 6
⊢ ((𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → (𝑧 = 𝑦 → 𝑧 = 𝑥)) |
4 | | ax7 1930 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝑧 = 𝑦 → 𝑥 = 𝑦)) |
5 | 3, 4 | syli 38 |
. . . . 5
⊢ ((𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → (𝑧 = 𝑦 → 𝑥 = 𝑦)) |
6 | 5 | com12 32 |
. . . 4
⊢ (𝑧 = 𝑦 → ((𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → 𝑥 = 𝑦)) |
7 | 2, 6 | eximii 1754 |
. . 3
⊢
∃𝑧((𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → 𝑥 = 𝑦) |
8 | 7 | 19.35i 1795 |
. 2
⊢
(∀𝑧(𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → ∃𝑧 𝑥 = 𝑦) |
9 | 4 | spsd 2045 |
. . . . 5
⊢ (𝑧 = 𝑥 → (∀𝑧 𝑧 = 𝑦 → 𝑥 = 𝑦)) |
10 | 9 | sps 2043 |
. . . 4
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑧 𝑧 = 𝑦 → 𝑥 = 𝑦)) |
11 | 10 | a1dd 48 |
. . 3
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑧 𝑧 = 𝑦 → (∃𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦))) |
12 | | nfeqf 2289 |
. . . . 5
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑥 = 𝑦) |
13 | 12 | 19.9d 2058 |
. . . 4
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∃𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
14 | 13 | ex 449 |
. . 3
⊢ (¬
∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (∃𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦))) |
15 | 11, 14 | bija 369 |
. 2
⊢
((∀𝑧 𝑧 = 𝑥 ↔ ∀𝑧 𝑧 = 𝑦) → (∃𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
16 | 1, 8, 15 | sylc 63 |
1
⊢
(∀𝑧(𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → 𝑥 = 𝑦) |