Step | Hyp | Ref
| Expression |
1 | | df-id 5489 |
. 2
⊢ I =
{〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} |
2 | | equcomi 2020 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
3 | 2 | opeq2d 4811 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑥〉) |
4 | 3 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑧 = 〈𝑥, 𝑦〉 ↔ 𝑧 = 〈𝑥, 𝑥〉)) |
5 | 4 | pm5.32ri 576 |
. . . . . . . . 9
⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦) ↔ (𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑦)) |
6 | 5 | exbii 1850 |
. . . . . . . 8
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦) ↔ ∃𝑦(𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑦)) |
7 | | ax6evr 2018 |
. . . . . . . . 9
⊢
∃𝑦 𝑥 = 𝑦 |
8 | | 19.42v 1957 |
. . . . . . . . 9
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑦) ↔ (𝑧 = 〈𝑥, 𝑥〉 ∧ ∃𝑦 𝑥 = 𝑦)) |
9 | 7, 8 | mpbiran2 707 |
. . . . . . . 8
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑦) ↔ 𝑧 = 〈𝑥, 𝑥〉) |
10 | 6, 9 | bitri 274 |
. . . . . . 7
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦) ↔ 𝑧 = 〈𝑥, 𝑥〉) |
11 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑥〉 → 𝑥 = 𝑥) |
12 | 11 | pm4.71i 560 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑥〉 ↔ (𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
13 | 10, 12 | bitri 274 |
. . . . . 6
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦) ↔ (𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
14 | 13 | exbii 1850 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦) ↔ ∃𝑥(𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
15 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → 𝑥 = 𝑢) |
16 | 15, 15 | opeq12d 4812 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → 〈𝑥, 𝑥〉 = 〈𝑢, 𝑢〉) |
17 | 16 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → (𝑧 = 〈𝑥, 𝑥〉 ↔ 𝑧 = 〈𝑢, 𝑢〉)) |
18 | 15, 15 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → (𝑥 = 𝑥 ↔ 𝑢 = 𝑢)) |
19 | 17, 18 | anbi12d 631 |
. . . . . 6
⊢ (𝑥 = 𝑢 → ((𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ (𝑧 = 〈𝑢, 𝑢〉 ∧ 𝑢 = 𝑢))) |
20 | 19 | exexw 2054 |
. . . . 5
⊢
(∃𝑥(𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑥∃𝑥(𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
21 | 14, 20 | bitri 274 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦) ↔ ∃𝑥∃𝑥(𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
22 | 21 | abbii 2808 |
. . 3
⊢ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)} = {𝑧 ∣ ∃𝑥∃𝑥(𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)} |
23 | | df-opab 5137 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)} |
24 | | df-opab 5137 |
. . 3
⊢
{〈𝑥, 𝑥〉 ∣ 𝑥 = 𝑥} = {𝑧 ∣ ∃𝑥∃𝑥(𝑧 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)} |
25 | 22, 23, 24 | 3eqtr4i 2776 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} = {〈𝑥, 𝑥〉 ∣ 𝑥 = 𝑥} |
26 | 1, 25 | eqtri 2766 |
1
⊢ I =
{〈𝑥, 𝑥〉 ∣ 𝑥 = 𝑥} |