Step | Hyp | Ref
| Expression |
1 | | equvinv 1959 |
. 2
⊢ (𝑥 = 𝑦 ↔ ∃𝑢(𝑢 = 𝑥 ∧ 𝑢 = 𝑦)) |
2 | | df-wl-clelv2 33380 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↔ ∀𝑡(𝑡 = 𝑥 → 𝑡 ∈ 𝐴)) |
3 | | equtrr 1949 |
. . . . . . 7
⊢ (𝑢 = 𝑥 → (𝑡 = 𝑢 → 𝑡 = 𝑥)) |
4 | 3 | imim1d 82 |
. . . . . 6
⊢ (𝑢 = 𝑥 → ((𝑡 = 𝑥 → 𝑡 ∈ 𝐴) → (𝑡 = 𝑢 → 𝑡 ∈ 𝐴))) |
5 | 4 | alimdv 1845 |
. . . . 5
⊢ (𝑢 = 𝑥 → (∀𝑡(𝑡 = 𝑥 → 𝑡 ∈ 𝐴) → ∀𝑡(𝑡 = 𝑢 → 𝑡 ∈ 𝐴))) |
6 | 2, 5 | syl5bi 232 |
. . . 4
⊢ (𝑢 = 𝑥 → (𝑥 ∈ 𝐴 → ∀𝑡(𝑡 = 𝑢 → 𝑡 ∈ 𝐴))) |
7 | | equeuclr 1950 |
. . . . . . 7
⊢ (𝑢 = 𝑦 → (𝑡 = 𝑦 → 𝑡 = 𝑢)) |
8 | 7 | imim1d 82 |
. . . . . 6
⊢ (𝑢 = 𝑦 → ((𝑡 = 𝑢 → 𝑡 ∈ 𝐴) → (𝑡 = 𝑦 → 𝑡 ∈ 𝐴))) |
9 | 8 | alimdv 1845 |
. . . . 5
⊢ (𝑢 = 𝑦 → (∀𝑡(𝑡 = 𝑢 → 𝑡 ∈ 𝐴) → ∀𝑡(𝑡 = 𝑦 → 𝑡 ∈ 𝐴))) |
10 | | df-wl-clelv2 33380 |
. . . . 5
⊢ (𝑦 ∈ 𝐴 ↔ ∀𝑡(𝑡 = 𝑦 → 𝑡 ∈ 𝐴)) |
11 | 9, 10 | syl6ibr 242 |
. . . 4
⊢ (𝑢 = 𝑦 → (∀𝑡(𝑡 = 𝑢 → 𝑡 ∈ 𝐴) → 𝑦 ∈ 𝐴)) |
12 | 6, 11 | sylan9 689 |
. . 3
⊢ ((𝑢 = 𝑥 ∧ 𝑢 = 𝑦) → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴)) |
13 | 12 | exlimiv 1858 |
. 2
⊢
(∃𝑢(𝑢 = 𝑥 ∧ 𝑢 = 𝑦) → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴)) |
14 | 1, 13 | sylbi 207 |
1
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴)) |