Step | Hyp | Ref
| Expression |
1 | | nfa1 1539 |
. . . 4
⊢
Ⅎ𝑥∀𝑥 𝐴 = 𝐶 |
2 | | nfra1 2506 |
. . . 4
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 = 𝐷 |
3 | 1, 2 | nfan 1563 |
. . 3
⊢
Ⅎ𝑥(∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) |
4 | | nfv 1526 |
. . 3
⊢
Ⅎ𝑦(∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) |
5 | | rsp 2522 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐷 → (𝑥 ∈ 𝐴 → 𝐵 = 𝐷)) |
6 | 5 | imp 124 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 𝐵 = 𝐷 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) |
7 | 6 | eqeq2d 2187 |
. . . . 5
⊢
((∀𝑥 ∈
𝐴 𝐵 = 𝐷 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑦 = 𝐷)) |
8 | 7 | pm5.32da 452 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐷 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷))) |
9 | | sp 1509 |
. . . . . 6
⊢
(∀𝑥 𝐴 = 𝐶 → 𝐴 = 𝐶) |
10 | 9 | eleq2d 2245 |
. . . . 5
⊢
(∀𝑥 𝐴 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶)) |
11 | 10 | anbi1d 465 |
. . . 4
⊢
(∀𝑥 𝐴 = 𝐶 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷))) |
12 | 8, 11 | sylan9bbr 463 |
. . 3
⊢
((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷))) |
13 | 3, 4, 12 | opabbid 4063 |
. 2
⊢
((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)}) |
14 | | df-mpt 4061 |
. 2
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
15 | | df-mpt 4061 |
. 2
⊢ (𝑥 ∈ 𝐶 ↦ 𝐷) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)} |
16 | 13, 14, 15 | 3eqtr4g 2233 |
1
⊢
((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |