Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . 5
⊢
Ⅎ𝑣∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) |
2 | | nfv 1918 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑤 = ⟨𝑣, 𝑦⟩ |
3 | | nfs1v 2154 |
. . . . . . 7
⊢
Ⅎ𝑥[𝑣 / 𝑥]𝜑 |
4 | 2, 3 | nfan 1903 |
. . . . . 6
⊢
Ⅎ𝑥(𝑤 = ⟨𝑣, 𝑦⟩ ∧ [𝑣 / 𝑥]𝜑) |
5 | 4 | nfex 2318 |
. . . . 5
⊢
Ⅎ𝑥∃𝑦(𝑤 = ⟨𝑣, 𝑦⟩ ∧ [𝑣 / 𝑥]𝜑) |
6 | | opeq1 4874 |
. . . . . . . 8
⊢ (𝑥 = 𝑣 → ⟨𝑥, 𝑦⟩ = ⟨𝑣, 𝑦⟩) |
7 | 6 | eqeq2d 2744 |
. . . . . . 7
⊢ (𝑥 = 𝑣 → (𝑤 = ⟨𝑥, 𝑦⟩ ↔ 𝑤 = ⟨𝑣, 𝑦⟩)) |
8 | | sbequ12 2244 |
. . . . . . 7
⊢ (𝑥 = 𝑣 → (𝜑 ↔ [𝑣 / 𝑥]𝜑)) |
9 | 7, 8 | anbi12d 632 |
. . . . . 6
⊢ (𝑥 = 𝑣 → ((𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (𝑤 = ⟨𝑣, 𝑦⟩ ∧ [𝑣 / 𝑥]𝜑))) |
10 | 9 | exbidv 1925 |
. . . . 5
⊢ (𝑥 = 𝑣 → (∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑦(𝑤 = ⟨𝑣, 𝑦⟩ ∧ [𝑣 / 𝑥]𝜑))) |
11 | 1, 5, 10 | cbvexv1 2339 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑣∃𝑦(𝑤 = ⟨𝑣, 𝑦⟩ ∧ [𝑣 / 𝑥]𝜑)) |
12 | | nfv 1918 |
. . . . . . 7
⊢
Ⅎ𝑧 𝑤 = ⟨𝑣, 𝑦⟩ |
13 | | cbvopab1.1 |
. . . . . . . 8
⊢
Ⅎ𝑧𝜑 |
14 | 13 | nfsbv 2324 |
. . . . . . 7
⊢
Ⅎ𝑧[𝑣 / 𝑥]𝜑 |
15 | 12, 14 | nfan 1903 |
. . . . . 6
⊢
Ⅎ𝑧(𝑤 = ⟨𝑣, 𝑦⟩ ∧ [𝑣 / 𝑥]𝜑) |
16 | 15 | nfex 2318 |
. . . . 5
⊢
Ⅎ𝑧∃𝑦(𝑤 = ⟨𝑣, 𝑦⟩ ∧ [𝑣 / 𝑥]𝜑) |
17 | | nfv 1918 |
. . . . 5
⊢
Ⅎ𝑣∃𝑦(𝑤 = ⟨𝑧, 𝑦⟩ ∧ 𝜓) |
18 | | opeq1 4874 |
. . . . . . . 8
⊢ (𝑣 = 𝑧 → ⟨𝑣, 𝑦⟩ = ⟨𝑧, 𝑦⟩) |
19 | 18 | eqeq2d 2744 |
. . . . . . 7
⊢ (𝑣 = 𝑧 → (𝑤 = ⟨𝑣, 𝑦⟩ ↔ 𝑤 = ⟨𝑧, 𝑦⟩)) |
20 | | cbvopab1.2 |
. . . . . . . 8
⊢
Ⅎ𝑥𝜓 |
21 | | cbvopab1.3 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) |
22 | 20, 21 | sbhypf 3539 |
. . . . . . 7
⊢ (𝑣 = 𝑧 → ([𝑣 / 𝑥]𝜑 ↔ 𝜓)) |
23 | 19, 22 | anbi12d 632 |
. . . . . 6
⊢ (𝑣 = 𝑧 → ((𝑤 = ⟨𝑣, 𝑦⟩ ∧ [𝑣 / 𝑥]𝜑) ↔ (𝑤 = ⟨𝑧, 𝑦⟩ ∧ 𝜓))) |
24 | 23 | exbidv 1925 |
. . . . 5
⊢ (𝑣 = 𝑧 → (∃𝑦(𝑤 = ⟨𝑣, 𝑦⟩ ∧ [𝑣 / 𝑥]𝜑) ↔ ∃𝑦(𝑤 = ⟨𝑧, 𝑦⟩ ∧ 𝜓))) |
25 | 16, 17, 24 | cbvexv1 2339 |
. . . 4
⊢
(∃𝑣∃𝑦(𝑤 = ⟨𝑣, 𝑦⟩ ∧ [𝑣 / 𝑥]𝜑) ↔ ∃𝑧∃𝑦(𝑤 = ⟨𝑧, 𝑦⟩ ∧ 𝜓)) |
26 | 11, 25 | bitri 275 |
. . 3
⊢
(∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑧∃𝑦(𝑤 = ⟨𝑧, 𝑦⟩ ∧ 𝜓)) |
27 | 26 | abbii 2803 |
. 2
⊢ {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} = {𝑤 ∣ ∃𝑧∃𝑦(𝑤 = ⟨𝑧, 𝑦⟩ ∧ 𝜓)} |
28 | | df-opab 5212 |
. 2
⊢
{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} |
29 | | df-opab 5212 |
. 2
⊢
{⟨𝑧, 𝑦⟩ ∣ 𝜓} = {𝑤 ∣ ∃𝑧∃𝑦(𝑤 = ⟨𝑧, 𝑦⟩ ∧ 𝜓)} |
30 | 27, 28, 29 | 3eqtr4i 2771 |
1
⊢
{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓} |