Step | Hyp | Ref
| Expression |
1 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑥 𝑤 = 〈𝑡, 𝑢〉 |
2 | | dfoprab4f.x |
. . . . . 6
⊢
Ⅎ𝑥𝜑 |
3 | | nfs1v 2425 |
. . . . . 6
⊢
Ⅎ𝑥[𝑡 / 𝑥][𝑢 / 𝑦]𝜓 |
4 | 2, 3 | nfbi 1821 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓) |
5 | 1, 4 | nfim 1813 |
. . . 4
⊢
Ⅎ𝑥(𝑤 = 〈𝑡, 𝑢〉 → (𝜑 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓)) |
6 | | opeq1 4340 |
. . . . . 6
⊢ (𝑥 = 𝑡 → 〈𝑥, 𝑢〉 = 〈𝑡, 𝑢〉) |
7 | 6 | eqeq2d 2620 |
. . . . 5
⊢ (𝑥 = 𝑡 → (𝑤 = 〈𝑥, 𝑢〉 ↔ 𝑤 = 〈𝑡, 𝑢〉)) |
8 | | sbequ12 2097 |
. . . . . 6
⊢ (𝑥 = 𝑡 → ([𝑢 / 𝑦]𝜓 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓)) |
9 | 8 | bibi2d 331 |
. . . . 5
⊢ (𝑥 = 𝑡 → ((𝜑 ↔ [𝑢 / 𝑦]𝜓) ↔ (𝜑 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓))) |
10 | 7, 9 | imbi12d 333 |
. . . 4
⊢ (𝑥 = 𝑡 → ((𝑤 = 〈𝑥, 𝑢〉 → (𝜑 ↔ [𝑢 / 𝑦]𝜓)) ↔ (𝑤 = 〈𝑡, 𝑢〉 → (𝜑 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓)))) |
11 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑦 𝑤 = 〈𝑥, 𝑢〉 |
12 | | dfoprab4f.y |
. . . . . . 7
⊢
Ⅎ𝑦𝜑 |
13 | | nfs1v 2425 |
. . . . . . 7
⊢
Ⅎ𝑦[𝑢 / 𝑦]𝜓 |
14 | 12, 13 | nfbi 1821 |
. . . . . 6
⊢
Ⅎ𝑦(𝜑 ↔ [𝑢 / 𝑦]𝜓) |
15 | 11, 14 | nfim 1813 |
. . . . 5
⊢
Ⅎ𝑦(𝑤 = 〈𝑥, 𝑢〉 → (𝜑 ↔ [𝑢 / 𝑦]𝜓)) |
16 | | opeq2 4341 |
. . . . . . 7
⊢ (𝑦 = 𝑢 → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑢〉) |
17 | 16 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑦 = 𝑢 → (𝑤 = 〈𝑥, 𝑦〉 ↔ 𝑤 = 〈𝑥, 𝑢〉)) |
18 | | sbequ12 2097 |
. . . . . . 7
⊢ (𝑦 = 𝑢 → (𝜓 ↔ [𝑢 / 𝑦]𝜓)) |
19 | 18 | bibi2d 331 |
. . . . . 6
⊢ (𝑦 = 𝑢 → ((𝜑 ↔ 𝜓) ↔ (𝜑 ↔ [𝑢 / 𝑦]𝜓))) |
20 | 17, 19 | imbi12d 333 |
. . . . 5
⊢ (𝑦 = 𝑢 → ((𝑤 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ↔ (𝑤 = 〈𝑥, 𝑢〉 → (𝜑 ↔ [𝑢 / 𝑦]𝜓)))) |
21 | | dfoprab4f.1 |
. . . . 5
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) |
22 | 15, 20, 21 | chvar 2250 |
. . . 4
⊢ (𝑤 = 〈𝑥, 𝑢〉 → (𝜑 ↔ [𝑢 / 𝑦]𝜓)) |
23 | 5, 10, 22 | chvar 2250 |
. . 3
⊢ (𝑤 = 〈𝑡, 𝑢〉 → (𝜑 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓)) |
24 | 23 | dfoprab4 7116 |
. 2
⊢
{〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {〈〈𝑡, 𝑢〉, 𝑧〉 ∣ ((𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓)} |
25 | | nfv 1830 |
. . 3
⊢
Ⅎ𝑡((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) |
26 | | nfv 1830 |
. . 3
⊢
Ⅎ𝑢((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) |
27 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑥(𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) |
28 | 27, 3 | nfan 1816 |
. . 3
⊢
Ⅎ𝑥((𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓) |
29 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑦(𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) |
30 | 13 | nfsb 2428 |
. . . 4
⊢
Ⅎ𝑦[𝑡 / 𝑥][𝑢 / 𝑦]𝜓 |
31 | 29, 30 | nfan 1816 |
. . 3
⊢
Ⅎ𝑦((𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓) |
32 | | eleq1 2676 |
. . . . 5
⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)) |
33 | | eleq1 2676 |
. . . . 5
⊢ (𝑦 = 𝑢 → (𝑦 ∈ 𝐵 ↔ 𝑢 ∈ 𝐵)) |
34 | 32, 33 | bi2anan9 913 |
. . . 4
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑢) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵))) |
35 | 18, 8 | sylan9bbr 733 |
. . . 4
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑢) → (𝜓 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓)) |
36 | 34, 35 | anbi12d 743 |
. . 3
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑢) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) ↔ ((𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓))) |
37 | 25, 26, 28, 31, 36 | cbvoprab12 6627 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)} = {〈〈𝑡, 𝑢〉, 𝑧〉 ∣ ((𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓)} |
38 | 24, 37 | eqtr4i 2635 |
1
⊢
{〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)} |