Step | Hyp | Ref
| Expression |
1 | | velsn 4585 |
. . . . 5
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
2 | 1 | bicomi 226 |
. . . 4
⊢ (𝑥 = 𝐴 ↔ 𝑥 ∈ {𝐴}) |
3 | 2 | anbi1i 625 |
. . 3
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)) |
4 | 3 | opabbii 5135 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)} |
5 | | velsn 4585 |
. . . . 5
⊢ (𝑝 ∈ {〈𝐴, 𝐶〉} ↔ 𝑝 = 〈𝐴, 𝐶〉) |
6 | | eqidd 2824 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 = 𝐴) |
7 | | eqidd 2824 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 = 𝐶) |
8 | | sbcan 3823 |
. . . . . . . . . . 11
⊢
([𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ([𝐶 / 𝑦]𝑥 = 𝐴 ∧ [𝐶 / 𝑦]𝑦 = 𝐵)) |
9 | | fmptsnd.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ 𝑊) |
10 | | sbcg 3849 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝑊 → ([𝐶 / 𝑦]𝑥 = 𝐴 ↔ 𝑥 = 𝐴)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ([𝐶 / 𝑦]𝑥 = 𝐴 ↔ 𝑥 = 𝐴)) |
12 | | eqsbc3 3819 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝑊 → ([𝐶 / 𝑦]𝑦 = 𝐵 ↔ 𝐶 = 𝐵)) |
13 | 9, 12 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ([𝐶 / 𝑦]𝑦 = 𝐵 ↔ 𝐶 = 𝐵)) |
14 | 11, 13 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝜑 → (([𝐶 / 𝑦]𝑥 = 𝐴 ∧ [𝐶 / 𝑦]𝑦 = 𝐵) ↔ (𝑥 = 𝐴 ∧ 𝐶 = 𝐵))) |
15 | 8, 14 | syl5bb 285 |
. . . . . . . . . 10
⊢ (𝜑 → ([𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 = 𝐴 ∧ 𝐶 = 𝐵))) |
16 | 15 | sbcbidv 3829 |
. . . . . . . . 9
⊢ (𝜑 → ([𝐴 / 𝑥][𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ [𝐴 / 𝑥](𝑥 = 𝐴 ∧ 𝐶 = 𝐵))) |
17 | | fmptsnd.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
18 | | eqeq1 2827 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (𝑥 = 𝐴 ↔ 𝐴 = 𝐴)) |
19 | 18 | adantl 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑥 = 𝐴 ↔ 𝐴 = 𝐴)) |
20 | | fmptsnd.1 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) |
21 | 20 | eqeq2d 2834 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝐶 = 𝐵 ↔ 𝐶 = 𝐶)) |
22 | 19, 21 | anbi12d 632 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝑥 = 𝐴 ∧ 𝐶 = 𝐵) ↔ (𝐴 = 𝐴 ∧ 𝐶 = 𝐶))) |
23 | 17, 22 | sbcied 3816 |
. . . . . . . . 9
⊢ (𝜑 → ([𝐴 / 𝑥](𝑥 = 𝐴 ∧ 𝐶 = 𝐵) ↔ (𝐴 = 𝐴 ∧ 𝐶 = 𝐶))) |
24 | 16, 23 | bitrd 281 |
. . . . . . . 8
⊢ (𝜑 → ([𝐴 / 𝑥][𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝐴 = 𝐴 ∧ 𝐶 = 𝐶))) |
25 | 6, 7, 24 | mpbir2and 711 |
. . . . . . 7
⊢ (𝜑 → [𝐴 / 𝑥][𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
26 | | opelopabsb 5419 |
. . . . . . 7
⊢
(〈𝐴, 𝐶〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} ↔ [𝐴 / 𝑥][𝐶 / 𝑦](𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
27 | 25, 26 | sylibr 236 |
. . . . . 6
⊢ (𝜑 → 〈𝐴, 𝐶〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)}) |
28 | | eleq1 2902 |
. . . . . 6
⊢ (𝑝 = 〈𝐴, 𝐶〉 → (𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} ↔ 〈𝐴, 𝐶〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
29 | 27, 28 | syl5ibrcom 249 |
. . . . 5
⊢ (𝜑 → (𝑝 = 〈𝐴, 𝐶〉 → 𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
30 | 5, 29 | syl5bi 244 |
. . . 4
⊢ (𝜑 → (𝑝 ∈ {〈𝐴, 𝐶〉} → 𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
31 | | elopab 5416 |
. . . . 5
⊢ (𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} ↔ ∃𝑥∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵))) |
32 | | opeq12 4807 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
33 | 32 | adantl 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
34 | 33 | eqeq2d 2834 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑝 = 〈𝑥, 𝑦〉 ↔ 𝑝 = 〈𝐴, 𝐵〉)) |
35 | 20 | adantrr 715 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝐵 = 𝐶) |
36 | 35 | opeq2d 4812 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 〈𝐴, 𝐵〉 = 〈𝐴, 𝐶〉) |
37 | | opex 5358 |
. . . . . . . . . . . 12
⊢
〈𝐴, 𝐶〉 ∈ V |
38 | 37 | snid 4603 |
. . . . . . . . . . 11
⊢
〈𝐴, 𝐶〉 ∈ {〈𝐴, 𝐶〉} |
39 | 36, 38 | eqeltrdi 2923 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 〈𝐴, 𝐵〉 ∈ {〈𝐴, 𝐶〉}) |
40 | | eleq1 2902 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝐴, 𝐵〉 → (𝑝 ∈ {〈𝐴, 𝐶〉} ↔ 〈𝐴, 𝐵〉 ∈ {〈𝐴, 𝐶〉})) |
41 | 39, 40 | syl5ibrcom 249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑝 = 〈𝐴, 𝐵〉 → 𝑝 ∈ {〈𝐴, 𝐶〉})) |
42 | 34, 41 | sylbid 242 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑝 = 〈𝑥, 𝑦〉 → 𝑝 ∈ {〈𝐴, 𝐶〉})) |
43 | 42 | ex 415 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑝 = 〈𝑥, 𝑦〉 → 𝑝 ∈ {〈𝐴, 𝐶〉}))) |
44 | 43 | impcomd 414 |
. . . . . 6
⊢ (𝜑 → ((𝑝 = 〈𝑥, 𝑦〉 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑝 ∈ {〈𝐴, 𝐶〉})) |
45 | 44 | exlimdvv 1935 |
. . . . 5
⊢ (𝜑 → (∃𝑥∃𝑦(𝑝 = 〈𝑥, 𝑦〉 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑝 ∈ {〈𝐴, 𝐶〉})) |
46 | 31, 45 | syl5bi 244 |
. . . 4
⊢ (𝜑 → (𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)} → 𝑝 ∈ {〈𝐴, 𝐶〉})) |
47 | 30, 46 | impbid 214 |
. . 3
⊢ (𝜑 → (𝑝 ∈ {〈𝐴, 𝐶〉} ↔ 𝑝 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)})) |
48 | 47 | eqrdv 2821 |
. 2
⊢ (𝜑 → {〈𝐴, 𝐶〉} = {〈𝑥, 𝑦〉 ∣ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)}) |
49 | | df-mpt 5149 |
. . 3
⊢ (𝑥 ∈ {𝐴} ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)} |
50 | 49 | a1i 11 |
. 2
⊢ (𝜑 → (𝑥 ∈ {𝐴} ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝐴} ∧ 𝑦 = 𝐵)}) |
51 | 4, 48, 50 | 3eqtr4a 2884 |
1
⊢ (𝜑 → {〈𝐴, 𝐶〉} = (𝑥 ∈ {𝐴} ↦ 𝐵)) |