Step | Hyp | Ref
| Expression |
1 | | velsn 4603 |
. . . . 5
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
2 | 1 | bicomi 223 |
. . . 4
⊢ (𝑥 = 𝐴 ↔ 𝑥 ∈ {𝐴}) |
3 | 2 | anbi1i 625 |
. . 3
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)) |
4 | 3 | opabbii 5173 |
. 2
⊢
{⟨𝑥, 𝑦⟩ ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)} |
5 | | velsn 4603 |
. . . . 5
⊢ (𝑝 ∈ {⟨𝐴, 𝐶⟩} ↔ 𝑝 = ⟨𝐴, 𝐶⟩) |
6 | | eqidd 2734 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 = 𝐴) |
7 | | eqidd 2734 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 = 𝐶) |
8 | | sbcan 3792 |
. . . . . . . . . . 11
⊢
([𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ([𝐶 / 𝑦]𝑥 = 𝐴 ∧ [𝐶 / 𝑦]𝑦 = 𝐵)) |
9 | | fmptsnd.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ 𝑊) |
10 | | sbcg 3819 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝑊 → ([𝐶 / 𝑦]𝑥 = 𝐴 ↔ 𝑥 = 𝐴)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ([𝐶 / 𝑦]𝑥 = 𝐴 ↔ 𝑥 = 𝐴)) |
12 | | eqsbc1 3789 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝑊 → ([𝐶 / 𝑦]𝑦 = 𝐵 ↔ 𝐶 = 𝐵)) |
13 | 9, 12 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ([𝐶 / 𝑦]𝑦 = 𝐵 ↔ 𝐶 = 𝐵)) |
14 | 11, 13 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝜑 → (([𝐶 / 𝑦]𝑥 = 𝐴 ∧ [𝐶 / 𝑦]𝑦 = 𝐵) ↔ (𝑥 = 𝐴 ∧ 𝐶 = 𝐵))) |
15 | 8, 14 | bitrid 283 |
. . . . . . . . . 10
⊢ (𝜑 → ([𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 = 𝐴 ∧ 𝐶 = 𝐵))) |
16 | 15 | sbcbidv 3799 |
. . . . . . . . 9
⊢ (𝜑 → ([𝐴 / 𝑥][𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ [𝐴 / 𝑥](𝑥 = 𝐴 ∧ 𝐶 = 𝐵))) |
17 | | fmptsnd.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
18 | | eqeq1 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (𝑥 = 𝐴 ↔ 𝐴 = 𝐴)) |
19 | 18 | adantl 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑥 = 𝐴 ↔ 𝐴 = 𝐴)) |
20 | | fmptsnd.1 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) |
21 | 20 | eqeq2d 2744 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝐶 = 𝐵 ↔ 𝐶 = 𝐶)) |
22 | 19, 21 | anbi12d 632 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝑥 = 𝐴 ∧ 𝐶 = 𝐵) ↔ (𝐴 = 𝐴 ∧ 𝐶 = 𝐶))) |
23 | 17, 22 | sbcied 3785 |
. . . . . . . . 9
⊢ (𝜑 → ([𝐴 / 𝑥](𝑥 = 𝐴 ∧ 𝐶 = 𝐵) ↔ (𝐴 = 𝐴 ∧ 𝐶 = 𝐶))) |
24 | 16, 23 | bitrd 279 |
. . . . . . . 8
⊢ (𝜑 → ([𝐴 / 𝑥][𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝐴 = 𝐴 ∧ 𝐶 = 𝐶))) |
25 | 6, 7, 24 | mpbir2and 712 |
. . . . . . 7
⊢ (𝜑 → [𝐴 / 𝑥][𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
26 | | opelopabsb 5488 |
. . . . . . 7
⊢
(⟨𝐴, 𝐶⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} ↔ [𝐴 / 𝑥][𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
27 | 25, 26 | sylibr 233 |
. . . . . 6
⊢ (𝜑 → ⟨𝐴, 𝐶⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)}) |
28 | | eleq1 2822 |
. . . . . 6
⊢ (𝑝 = ⟨𝐴, 𝐶⟩ → (𝑝 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} ↔ ⟨𝐴, 𝐶⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
29 | 27, 28 | syl5ibrcom 247 |
. . . . 5
⊢ (𝜑 → (𝑝 = ⟨𝐴, 𝐶⟩ → 𝑝 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
30 | 5, 29 | biimtrid 241 |
. . . 4
⊢ (𝜑 → (𝑝 ∈ {⟨𝐴, 𝐶⟩} → 𝑝 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
31 | | elopab 5485 |
. . . . 5
⊢ (𝑝 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} ↔ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵))) |
32 | | opeq12 4833 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩) |
33 | 32 | adantl 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩) |
34 | 33 | eqeq2d 2744 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑝 = ⟨𝑥, 𝑦⟩ ↔ 𝑝 = ⟨𝐴, 𝐵⟩)) |
35 | 20 | adantrr 716 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝐵 = 𝐶) |
36 | 35 | opeq2d 4838 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐶⟩) |
37 | | opex 5422 |
. . . . . . . . . . . 12
⊢
⟨𝐴, 𝐶⟩ ∈ V |
38 | 37 | snid 4623 |
. . . . . . . . . . 11
⊢
⟨𝐴, 𝐶⟩ ∈ {⟨𝐴, 𝐶⟩} |
39 | 36, 38 | eqeltrdi 2842 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ⟨𝐴, 𝐵⟩ ∈ {⟨𝐴, 𝐶⟩}) |
40 | | eleq1 2822 |
. . . . . . . . . 10
⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (𝑝 ∈ {⟨𝐴, 𝐶⟩} ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝐴, 𝐶⟩})) |
41 | 39, 40 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑝 = ⟨𝐴, 𝐵⟩ → 𝑝 ∈ {⟨𝐴, 𝐶⟩})) |
42 | 34, 41 | sylbid 239 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑝 = ⟨𝑥, 𝑦⟩ → 𝑝 ∈ {⟨𝐴, 𝐶⟩})) |
43 | 42 | ex 414 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑝 = ⟨𝑥, 𝑦⟩ → 𝑝 ∈ {⟨𝐴, 𝐶⟩}))) |
44 | 43 | impcomd 413 |
. . . . . 6
⊢ (𝜑 → ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑝 ∈ {⟨𝐴, 𝐶⟩})) |
45 | 44 | exlimdvv 1938 |
. . . . 5
⊢ (𝜑 → (∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑝 ∈ {⟨𝐴, 𝐶⟩})) |
46 | 31, 45 | biimtrid 241 |
. . . 4
⊢ (𝜑 → (𝑝 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} → 𝑝 ∈ {⟨𝐴, 𝐶⟩})) |
47 | 30, 46 | impbid 211 |
. . 3
⊢ (𝜑 → (𝑝 ∈ {⟨𝐴, 𝐶⟩} ↔ 𝑝 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
48 | 47 | eqrdv 2731 |
. 2
⊢ (𝜑 → {⟨𝐴, 𝐶⟩} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)}) |
49 | | df-mpt 5190 |
. . 3
⊢ (𝑥 ∈ {𝐴} ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)} |
50 | 49 | a1i 11 |
. 2
⊢ (𝜑 → (𝑥 ∈ {𝐴} ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)}) |
51 | 4, 48, 50 | 3eqtr4a 2799 |
1
⊢ (𝜑 → {⟨𝐴, 𝐶⟩} = (𝑥 ∈ {𝐴} ↦ 𝐵)) |