Step | Hyp | Ref
| Expression |
1 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑤 𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 |
2 | | cbvoprab2.1 |
. . . . . . 7
⊢
Ⅎ𝑤𝜑 |
3 | 1, 2 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑤(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
4 | 3 | nfex 2327 |
. . . . 5
⊢
Ⅎ𝑤∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
5 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑦 𝑣 = 〈〈𝑥, 𝑤〉, 𝑧〉 |
6 | | cbvoprab2.2 |
. . . . . . 7
⊢
Ⅎ𝑦𝜓 |
7 | 5, 6 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑦(𝑣 = 〈〈𝑥, 𝑤〉, 𝑧〉 ∧ 𝜓) |
8 | 7 | nfex 2327 |
. . . . 5
⊢
Ⅎ𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑤〉, 𝑧〉 ∧ 𝜓) |
9 | | opeq2 4771 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑤〉) |
10 | 9 | opeq1d 4777 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → 〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑥, 𝑤〉, 𝑧〉) |
11 | 10 | eqeq2d 2750 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 𝑣 = 〈〈𝑥, 𝑤〉, 𝑧〉)) |
12 | | cbvoprab2.3 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜓)) |
13 | 11, 12 | anbi12d 634 |
. . . . . 6
⊢ (𝑦 = 𝑤 → ((𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ (𝑣 = 〈〈𝑥, 𝑤〉, 𝑧〉 ∧ 𝜓))) |
14 | 13 | exbidv 1928 |
. . . . 5
⊢ (𝑦 = 𝑤 → (∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑧(𝑣 = 〈〈𝑥, 𝑤〉, 𝑧〉 ∧ 𝜓))) |
15 | 4, 8, 14 | cbvexv1 2345 |
. . . 4
⊢
(∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑤∃𝑧(𝑣 = 〈〈𝑥, 𝑤〉, 𝑧〉 ∧ 𝜓)) |
16 | 15 | exbii 1854 |
. . 3
⊢
(∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑤∃𝑧(𝑣 = 〈〈𝑥, 𝑤〉, 𝑧〉 ∧ 𝜓)) |
17 | 16 | abbii 2804 |
. 2
⊢ {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} = {𝑣 ∣ ∃𝑥∃𝑤∃𝑧(𝑣 = 〈〈𝑥, 𝑤〉, 𝑧〉 ∧ 𝜓)} |
18 | | df-oprab 7187 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
19 | | df-oprab 7187 |
. 2
⊢
{〈〈𝑥,
𝑤〉, 𝑧〉 ∣ 𝜓} = {𝑣 ∣ ∃𝑥∃𝑤∃𝑧(𝑣 = 〈〈𝑥, 𝑤〉, 𝑧〉 ∧ 𝜓)} |
20 | 17, 18, 19 | 3eqtr4i 2772 |
1
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑤〉, 𝑧〉 ∣ 𝜓} |