Step | Hyp | Ref
| Expression |
1 | | velsn 4557 |
. . . . 5
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
2 | 1 | bicomi 227 |
. . . 4
⊢ (𝑥 = 𝐴 ↔ 𝑥 ∈ {𝐴}) |
3 | 2 | anbi1i 627 |
. . 3
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)) |
4 | 3 | opabbii 5120 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)} |
5 | | velsn 4557 |
. . . . 5
⊢ (𝑝 ∈ {〈𝐴, 𝐶〉} ↔ 𝑝 = 〈𝐴, 𝐶〉) |
6 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → 𝐴 = 𝐴) |
7 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → 𝐶 = 𝐶) |
8 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 = 𝐴 ↔ 𝐴 = 𝐴)) |
9 | 8 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐶) → (𝑥 = 𝐴 ↔ 𝐴 = 𝐴)) |
10 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐶 → (𝑦 = 𝐵 ↔ 𝐶 = 𝐵)) |
11 | | fmptsng.1 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) |
12 | 11 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐶 = 𝐵 ↔ 𝐶 = 𝐶)) |
13 | 10, 12 | sylan9bbr 514 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐶) → (𝑦 = 𝐵 ↔ 𝐶 = 𝐶)) |
14 | 9, 13 | anbi12d 634 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐶) → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝐴 = 𝐴 ∧ 𝐶 = 𝐶))) |
15 | 14 | opelopabga 5414 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (〈𝐴, 𝐶〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} ↔ (𝐴 = 𝐴 ∧ 𝐶 = 𝐶))) |
16 | 6, 7, 15 | mpbir2and 713 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → 〈𝐴, 𝐶〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)}) |
17 | | eleq1 2825 |
. . . . . 6
⊢ (𝑝 = 〈𝐴, 𝐶〉 → (𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} ↔ 〈𝐴, 𝐶〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
18 | 16, 17 | syl5ibrcom 250 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝑝 = 〈𝐴, 𝐶〉 → 𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
19 | 5, 18 | syl5bi 245 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝑝 ∈ {〈𝐴, 𝐶〉} → 𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
20 | | elopab 5408 |
. . . . 5
⊢ (𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} ↔ ∃𝑥∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵))) |
21 | | opeq12 4786 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
22 | 21 | eqeq2d 2748 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑝 = 〈𝑥, 𝑦〉 ↔ 𝑝 = 〈𝐴, 𝐵〉)) |
23 | 11 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐵 = 𝐶) |
24 | 23 | opeq2d 4791 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝐴, 𝐵〉 = 〈𝐴, 𝐶〉) |
25 | | opex 5348 |
. . . . . . . . . . . 12
⊢
〈𝐴, 𝐶〉 ∈ V |
26 | 25 | snid 4577 |
. . . . . . . . . . 11
⊢
〈𝐴, 𝐶〉 ∈ {〈𝐴, 𝐶〉} |
27 | 24, 26 | eqeltrdi 2846 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝐴, 𝐵〉 ∈ {〈𝐴, 𝐶〉}) |
28 | | eleq1 2825 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝐴, 𝐵〉 → (𝑝 ∈ {〈𝐴, 𝐶〉} ↔ 〈𝐴, 𝐵〉 ∈ {〈𝐴, 𝐶〉})) |
29 | 27, 28 | syl5ibrcom 250 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑝 = 〈𝐴, 𝐵〉 → 𝑝 ∈ {〈𝐴, 𝐶〉})) |
30 | 22, 29 | sylbid 243 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑝 = 〈𝑥, 𝑦〉 → 𝑝 ∈ {〈𝐴, 𝐶〉})) |
31 | 30 | impcom 411 |
. . . . . . 7
⊢ ((𝑝 = 〈𝑥, 𝑦〉 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑝 ∈ {〈𝐴, 𝐶〉}) |
32 | 31 | exlimivv 1940 |
. . . . . 6
⊢
(∃𝑥∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑝 ∈ {〈𝐴, 𝐶〉}) |
33 | 32 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑥∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑝 ∈ {〈𝐴, 𝐶〉})) |
34 | 20, 33 | syl5bi 245 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} → 𝑝 ∈ {〈𝐴, 𝐶〉})) |
35 | 19, 34 | impbid 215 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝑝 ∈ {〈𝐴, 𝐶〉} ↔ 𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
36 | 35 | eqrdv 2735 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → {〈𝐴, 𝐶〉} = {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)}) |
37 | | df-mpt 5136 |
. . 3
⊢ (𝑥 ∈ {𝐴} ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)} |
38 | 37 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝑥 ∈ {𝐴} ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)}) |
39 | 4, 36, 38 | 3eqtr4a 2804 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → {〈𝐴, 𝐶〉} = (𝑥 ∈ {𝐴} ↦ 𝐵)) |