Step | Hyp | Ref
| Expression |
1 | | nfv 1521 |
. . . 4
⊢
Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) |
2 | | cbvmptf.1 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
3 | 2 | nfcri 2306 |
. . . . 5
⊢
Ⅎ𝑥 𝑤 ∈ 𝐴 |
4 | | nfs1v 1932 |
. . . . 5
⊢
Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵 |
5 | 3, 4 | nfan 1558 |
. . . 4
⊢
Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
6 | | eleq1w 2231 |
. . . . 5
⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
7 | | sbequ12 1764 |
. . . . 5
⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵)) |
8 | 6, 7 | anbi12d 470 |
. . . 4
⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵))) |
9 | 1, 5, 8 | cbvopab1 4062 |
. . 3
⊢
{〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} |
10 | | cbvmptf.2 |
. . . . . 6
⊢
Ⅎ𝑦𝐴 |
11 | 10 | nfcri 2306 |
. . . . 5
⊢
Ⅎ𝑦 𝑤 ∈ 𝐴 |
12 | | cbvmptf.3 |
. . . . . . 7
⊢
Ⅎ𝑦𝐵 |
13 | 12 | nfeq2 2324 |
. . . . . 6
⊢
Ⅎ𝑦 𝑧 = 𝐵 |
14 | 13 | nfsb 1939 |
. . . . 5
⊢
Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵 |
15 | 11, 14 | nfan 1558 |
. . . 4
⊢
Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
16 | | nfv 1521 |
. . . 4
⊢
Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶) |
17 | | eleq1w 2231 |
. . . . 5
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
18 | | cbvmptf.4 |
. . . . . . 7
⊢
Ⅎ𝑥𝐶 |
19 | 18 | nfeq2 2324 |
. . . . . 6
⊢
Ⅎ𝑥 𝑧 = 𝐶 |
20 | | cbvmptf.5 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
21 | 20 | eqeq2d 2182 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
22 | 19, 21 | sbhypf 2779 |
. . . . 5
⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
23 | 17, 22 | anbi12d 470 |
. . . 4
⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶))) |
24 | 15, 16, 23 | cbvopab1 4062 |
. . 3
⊢
{〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
25 | 9, 24 | eqtri 2191 |
. 2
⊢
{〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
26 | | df-mpt 4052 |
. 2
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} |
27 | | df-mpt 4052 |
. 2
⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
28 | 25, 26, 27 | 3eqtr4i 2201 |
1
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |