Step | Hyp | Ref
| Expression |
1 | | nfv 1619 |
. . . . 5
⊢ Ⅎv∃y(w = 〈x, y〉 ∧ φ) |
2 | | nfv 1619 |
. . . . . . 7
⊢ Ⅎx w = 〈v, y〉 |
3 | | nfs1v 2106 |
. . . . . . 7
⊢ Ⅎx[v / x]φ |
4 | 2, 3 | nfan 1824 |
. . . . . 6
⊢ Ⅎx(w = 〈v, y〉 ∧ [v / x]φ) |
5 | 4 | nfex 1843 |
. . . . 5
⊢ Ⅎx∃y(w = 〈v, y〉 ∧ [v / x]φ) |
6 | | opeq1 4578 |
. . . . . . . 8
⊢ (x = v →
〈x,
y〉 =
〈v,
y〉) |
7 | 6 | eqeq2d 2364 |
. . . . . . 7
⊢ (x = v →
(w = 〈x, y〉 ↔ w = 〈v, y〉)) |
8 | | sbequ12 1919 |
. . . . . . 7
⊢ (x = v →
(φ ↔ [v / x]φ)) |
9 | 7, 8 | anbi12d 691 |
. . . . . 6
⊢ (x = v →
((w = 〈x, y〉 ∧ φ) ↔
(w = 〈v, y〉 ∧ [v / x]φ))) |
10 | 9 | exbidv 1626 |
. . . . 5
⊢ (x = v →
(∃y(w = 〈x, y〉 ∧ φ) ↔
∃y(w = 〈v, y〉 ∧ [v / x]φ))) |
11 | 1, 5, 10 | cbvex 1985 |
. . . 4
⊢ (∃x∃y(w = 〈x, y〉 ∧ φ) ↔ ∃v∃y(w = 〈v, y〉 ∧ [v / x]φ)) |
12 | | nfv 1619 |
. . . . . . 7
⊢ Ⅎz w = 〈v, y〉 |
13 | | cbvopab1.1 |
. . . . . . . 8
⊢ Ⅎzφ |
14 | 13 | nfsb 2109 |
. . . . . . 7
⊢ Ⅎz[v / x]φ |
15 | 12, 14 | nfan 1824 |
. . . . . 6
⊢ Ⅎz(w = 〈v, y〉 ∧ [v / x]φ) |
16 | 15 | nfex 1843 |
. . . . 5
⊢ Ⅎz∃y(w = 〈v, y〉 ∧ [v / x]φ) |
17 | | nfv 1619 |
. . . . 5
⊢ Ⅎv∃y(w = 〈z, y〉 ∧ ψ) |
18 | | opeq1 4578 |
. . . . . . . 8
⊢ (v = z →
〈v,
y〉 =
〈z,
y〉) |
19 | 18 | eqeq2d 2364 |
. . . . . . 7
⊢ (v = z →
(w = 〈v, y〉 ↔ w = 〈z, y〉)) |
20 | | sbequ 2060 |
. . . . . . . 8
⊢ (v = z →
([v / x]φ ↔
[z / x]φ)) |
21 | | cbvopab1.2 |
. . . . . . . . 9
⊢ Ⅎxψ |
22 | | cbvopab1.3 |
. . . . . . . . 9
⊢ (x = z →
(φ ↔ ψ)) |
23 | 21, 22 | sbie 2038 |
. . . . . . . 8
⊢ ([z / x]φ ↔ ψ) |
24 | 20, 23 | syl6bb 252 |
. . . . . . 7
⊢ (v = z →
([v / x]φ ↔
ψ)) |
25 | 19, 24 | anbi12d 691 |
. . . . . 6
⊢ (v = z →
((w = 〈v, y〉 ∧ [v / x]φ) ↔
(w = 〈z, y〉 ∧ ψ))) |
26 | 25 | exbidv 1626 |
. . . . 5
⊢ (v = z →
(∃y(w = 〈v, y〉 ∧ [v / x]φ) ↔
∃y(w = 〈z, y〉 ∧ ψ))) |
27 | 16, 17, 26 | cbvex 1985 |
. . . 4
⊢ (∃v∃y(w = 〈v, y〉 ∧ [v / x]φ) ↔ ∃z∃y(w = 〈z, y〉 ∧ ψ)) |
28 | 11, 27 | bitri 240 |
. . 3
⊢ (∃x∃y(w = 〈x, y〉 ∧ φ) ↔ ∃z∃y(w = 〈z, y〉 ∧ ψ)) |
29 | 28 | abbii 2465 |
. 2
⊢ {w ∣ ∃x∃y(w = 〈x, y〉 ∧ φ)} = {w
∣ ∃z∃y(w = 〈z, y〉 ∧ ψ)} |
30 | | df-opab 4623 |
. 2
⊢ {〈x, y〉 ∣ φ} =
{w ∣
∃x∃y(w = 〈x, y〉 ∧ φ)} |
31 | | df-opab 4623 |
. 2
⊢ {〈z, y〉 ∣ ψ} =
{w ∣
∃z∃y(w = 〈z, y〉 ∧ ψ)} |
32 | 29, 30, 31 | 3eqtr4i 2383 |
1
⊢ {〈x, y〉 ∣ φ} =
{〈z,
y〉 ∣ ψ} |