Step |
Hyp |
Ref |
Expression |
1 |
|
equtr |
⊢ ( 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → 𝑧 = 𝑦 ) ) |
2 |
|
equeuclr |
⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) ) |
3 |
2
|
anc2ri |
⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) ) |
4 |
1 3
|
syli |
⊢ ( 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) ) |
5 |
|
19.8a |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) |
6 |
4 5
|
syl6 |
⊢ ( 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) ) |
7 |
|
ax13 |
⊢ ( ¬ 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) |
8 |
|
ax6e |
⊢ ∃ 𝑧 𝑧 = 𝑦 |
9 |
8 3
|
eximii |
⊢ ∃ 𝑧 ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) |
10 |
9
|
19.35i |
⊢ ( ∀ 𝑧 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) |
11 |
7 10
|
syl6 |
⊢ ( ¬ 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) ) |
12 |
6 11
|
pm2.61i |
⊢ ( 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) |