Step | Hyp | Ref
| Expression |
1 | | df-id 4768 |
. 2
⊢ I = {⟨x, z⟩ ∣ x = z} |
2 | | ancom 437 |
. . . . . . . . . . 11
⊢ ((w = ⟨x, z⟩ ∧ x = z) ↔
(x = z
∧ w =
⟨x,
z⟩)) |
3 | | equcom 1680 |
. . . . . . . . . . . 12
⊢ (x = z ↔
z = x) |
4 | 3 | anbi1i 676 |
. . . . . . . . . . 11
⊢ ((x = z ∧ w = ⟨x, z⟩) ↔
(z = x
∧ w =
⟨x,
z⟩)) |
5 | 2, 4 | bitri 240 |
. . . . . . . . . 10
⊢ ((w = ⟨x, z⟩ ∧ x = z) ↔
(z = x
∧ w =
⟨x,
z⟩)) |
6 | 5 | exbii 1582 |
. . . . . . . . 9
⊢ (∃z(w = ⟨x, z⟩ ∧ x = z) ↔
∃z(z = x ∧ w = ⟨x, z⟩)) |
7 | | vex 2863 |
. . . . . . . . . 10
⊢ x ∈
V |
8 | | opeq2 4580 |
. . . . . . . . . . 11
⊢ (z = x →
⟨x,
z⟩ =
⟨x,
x⟩) |
9 | 8 | eqeq2d 2364 |
. . . . . . . . . 10
⊢ (z = x →
(w = ⟨x, z⟩ ↔ w = ⟨x, x⟩)) |
10 | 7, 9 | ceqsexv 2895 |
. . . . . . . . 9
⊢ (∃z(z = x ∧ w = ⟨x, z⟩) ↔
w = ⟨x, x⟩) |
11 | | equid 1676 |
. . . . . . . . . 10
⊢ x = x |
12 | 11 | biantru 491 |
. . . . . . . . 9
⊢ (w = ⟨x, x⟩ ↔ (w =
⟨x,
x⟩ ∧ x = x)) |
13 | 6, 10, 12 | 3bitri 262 |
. . . . . . . 8
⊢ (∃z(w = ⟨x, z⟩ ∧ x = z) ↔
(w = ⟨x, x⟩ ∧ x = x)) |
14 | 13 | exbii 1582 |
. . . . . . 7
⊢ (∃x∃z(w = ⟨x, z⟩ ∧ x = z) ↔
∃x(w = ⟨x, x⟩ ∧ x = x)) |
15 | | nfe1 1732 |
. . . . . . . 8
⊢ Ⅎx∃x(w = ⟨x, x⟩ ∧ x = x) |
16 | 15 | 19.9 1783 |
. . . . . . 7
⊢ (∃x∃x(w = ⟨x, x⟩ ∧ x = x) ↔
∃x(w = ⟨x, x⟩ ∧ x = x)) |
17 | 14, 16 | bitr4i 243 |
. . . . . 6
⊢ (∃x∃z(w = ⟨x, z⟩ ∧ x = z) ↔
∃x∃x(w = ⟨x, x⟩ ∧ x = x)) |
18 | | opeq2 4580 |
. . . . . . . . . . 11
⊢ (x = y →
⟨x,
x⟩ =
⟨x,
y⟩) |
19 | 18 | eqeq2d 2364 |
. . . . . . . . . 10
⊢ (x = y →
(w = ⟨x, x⟩ ↔ w = ⟨x, y⟩)) |
20 | | equequ2 1686 |
. . . . . . . . . 10
⊢ (x = y →
(x = x
↔ x = y)) |
21 | 19, 20 | anbi12d 691 |
. . . . . . . . 9
⊢ (x = y →
((w = ⟨x, x⟩ ∧ x = x) ↔ (w =
⟨x,
y⟩ ∧ x = y))) |
22 | 21 | sps 1754 |
. . . . . . . 8
⊢ (∀x x = y →
((w = ⟨x, x⟩ ∧ x = x) ↔ (w =
⟨x,
y⟩ ∧ x = y))) |
23 | 22 | drex1 1967 |
. . . . . . 7
⊢ (∀x x = y →
(∃x(w = ⟨x, x⟩ ∧ x = x) ↔ ∃y(w = ⟨x, y⟩ ∧ x = y))) |
24 | 23 | drex2 1968 |
. . . . . 6
⊢ (∀x x = y →
(∃x∃x(w = ⟨x, x⟩ ∧ x = x) ↔
∃x∃y(w = ⟨x, y⟩ ∧ x = y))) |
25 | 17, 24 | syl5bb 248 |
. . . . 5
⊢ (∀x x = y →
(∃x∃z(w = ⟨x, z⟩ ∧ x = z) ↔
∃x∃y(w = ⟨x, y⟩ ∧ x = y))) |
26 | | nfnae 1956 |
. . . . . 6
⊢ Ⅎx ¬ ∀x x = y |
27 | | nfnae 1956 |
. . . . . . 7
⊢ Ⅎy ¬ ∀x x = y |
28 | | nfcvd 2491 |
. . . . . . . . 9
⊢ (¬ ∀x x = y →
Ⅎyw) |
29 | | nfcvf2 2513 |
. . . . . . . . . 10
⊢ (¬ ∀x x = y →
Ⅎyx) |
30 | | nfcvd 2491 |
. . . . . . . . . 10
⊢ (¬ ∀x x = y →
Ⅎyz) |
31 | 29, 30 | nfopd 4606 |
. . . . . . . . 9
⊢ (¬ ∀x x = y →
Ⅎy⟨x, z⟩) |
32 | 28, 31 | nfeqd 2504 |
. . . . . . . 8
⊢ (¬ ∀x x = y →
Ⅎy w = ⟨x, z⟩) |
33 | 29, 30 | nfeqd 2504 |
. . . . . . . 8
⊢ (¬ ∀x x = y →
Ⅎy x = z) |
34 | 32, 33 | nfand 1822 |
. . . . . . 7
⊢ (¬ ∀x x = y →
Ⅎy(w = ⟨x, z⟩ ∧ x = z)) |
35 | | opeq2 4580 |
. . . . . . . . . 10
⊢ (z = y →
⟨x,
z⟩ =
⟨x,
y⟩) |
36 | 35 | eqeq2d 2364 |
. . . . . . . . 9
⊢ (z = y →
(w = ⟨x, z⟩ ↔ w = ⟨x, y⟩)) |
37 | | equequ2 1686 |
. . . . . . . . 9
⊢ (z = y →
(x = z
↔ x = y)) |
38 | 36, 37 | anbi12d 691 |
. . . . . . . 8
⊢ (z = y →
((w = ⟨x, z⟩ ∧ x = z) ↔ (w =
⟨x,
y⟩ ∧ x = y))) |
39 | 38 | a1i 10 |
. . . . . . 7
⊢ (¬ ∀x x = y →
(z = y
→ ((w = ⟨x, z⟩ ∧ x = z) ↔ (w =
⟨x,
y⟩ ∧ x = y)))) |
40 | 27, 34, 39 | cbvexd 2009 |
. . . . . 6
⊢ (¬ ∀x x = y →
(∃z(w = ⟨x, z⟩ ∧ x = z) ↔ ∃y(w = ⟨x, y⟩ ∧ x = y))) |
41 | 26, 40 | exbid 1773 |
. . . . 5
⊢ (¬ ∀x x = y →
(∃x∃z(w = ⟨x, z⟩ ∧ x = z) ↔
∃x∃y(w = ⟨x, y⟩ ∧ x = y))) |
42 | 25, 41 | pm2.61i 156 |
. . . 4
⊢ (∃x∃z(w = ⟨x, z⟩ ∧ x = z) ↔
∃x∃y(w = ⟨x, y⟩ ∧ x = y)) |
43 | 42 | abbii 2466 |
. . 3
⊢ {w ∣ ∃x∃z(w = ⟨x, z⟩ ∧ x = z)} =
{w ∣
∃x∃y(w = ⟨x, y⟩ ∧ x = y)} |
44 | | df-opab 4624 |
. . 3
⊢ {⟨x, z⟩ ∣ x = z} = {w ∣ ∃x∃z(w = ⟨x, z⟩ ∧ x = z)} |
45 | | df-opab 4624 |
. . 3
⊢ {⟨x, y⟩ ∣ x = y} = {w ∣ ∃x∃y(w = ⟨x, y⟩ ∧ x = y)} |
46 | 43, 44, 45 | 3eqtr4i 2383 |
. 2
⊢ {⟨x, z⟩ ∣ x = z} = {⟨x, y⟩ ∣ x = y} |
47 | 1, 46 | eqtri 2373 |
1
⊢ I = {⟨x, y⟩ ∣ x = y} |