Step | Hyp | Ref
| Expression |
1 | | df-rel 5045 |
. 2
⊢ (Rel
〈𝐴, 𝐵〉 ↔ 〈𝐴, 𝐵〉 ⊆ (V ×
V)) |
2 | | dfss2 3557 |
. . . . 5
⊢
(〈𝐴, 𝐵〉 ⊆ (V × V)
↔ ∀𝑧(𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V))) |
3 | | relop.1 |
. . . . . . . . . 10
⊢ 𝐴 ∈ V |
4 | | relop.2 |
. . . . . . . . . 10
⊢ 𝐵 ∈ V |
5 | 3, 4 | elop 4862 |
. . . . . . . . 9
⊢ (𝑧 ∈ 〈𝐴, 𝐵〉 ↔ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵})) |
6 | | elvv 5100 |
. . . . . . . . 9
⊢ (𝑧 ∈ (V × V) ↔
∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) |
7 | 5, 6 | imbi12i 339 |
. . . . . . . 8
⊢ ((𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉)) |
8 | | jaob 818 |
. . . . . . . 8
⊢ (((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ↔ ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
9 | 7, 8 | bitri 263 |
. . . . . . 7
⊢ ((𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
10 | 9 | albii 1737 |
. . . . . 6
⊢
(∀𝑧(𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V)) ↔ ∀𝑧((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
11 | | 19.26 1786 |
. . . . . 6
⊢
(∀𝑧((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
12 | 10, 11 | bitri 263 |
. . . . 5
⊢
(∀𝑧(𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
13 | 2, 12 | bitri 263 |
. . . 4
⊢
(〈𝐴, 𝐵〉 ⊆ (V × V)
↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
14 | | snex 4835 |
. . . . . . 7
⊢ {𝐴} ∈ V |
15 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑧 = {𝐴} → (𝑧 = {𝐴} ↔ {𝐴} = {𝐴})) |
16 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑧 = {𝐴} → (𝑧 = 〈𝑥, 𝑦〉 ↔ {𝐴} = 〈𝑥, 𝑦〉)) |
17 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ ({𝐴} = 〈𝑥, 𝑦〉 ↔ 〈𝑥, 𝑦〉 = {𝐴}) |
18 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
19 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
20 | 18, 19, 3 | opeqsn 4892 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 = {𝐴} ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥})) |
21 | 17, 20 | bitri 263 |
. . . . . . . . . 10
⊢ ({𝐴} = 〈𝑥, 𝑦〉 ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥})) |
22 | 16, 21 | syl6bb 275 |
. . . . . . . . 9
⊢ (𝑧 = {𝐴} → (𝑧 = 〈𝑥, 𝑦〉 ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))) |
23 | 22 | 2exbidv 1839 |
. . . . . . . 8
⊢ (𝑧 = {𝐴} → (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ↔ ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))) |
24 | 15, 23 | imbi12d 333 |
. . . . . . 7
⊢ (𝑧 = {𝐴} → ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ↔ ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})))) |
25 | 14, 24 | spcv 3272 |
. . . . . 6
⊢
(∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) → ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))) |
26 | | sneq 4135 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → {𝑤} = {𝑥}) |
27 | 26 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝐴 = {𝑤} ↔ 𝐴 = {𝑥})) |
28 | 27 | cbvexv 2263 |
. . . . . . 7
⊢
(∃𝑤 𝐴 = {𝑤} ↔ ∃𝑥 𝐴 = {𝑥}) |
29 | | ax6evr 1929 |
. . . . . . . . 9
⊢
∃𝑦 𝑥 = 𝑦 |
30 | | 19.41v 1901 |
. . . . . . . . 9
⊢
(∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ (∃𝑦 𝑥 = 𝑦 ∧ 𝐴 = {𝑥})) |
31 | 29, 30 | mpbiran 955 |
. . . . . . . 8
⊢
(∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ 𝐴 = {𝑥}) |
32 | 31 | exbii 1764 |
. . . . . . 7
⊢
(∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ ∃𝑥 𝐴 = {𝑥}) |
33 | | eqid 2610 |
. . . . . . . 8
⊢ {𝐴} = {𝐴} |
34 | 33 | a1bi 351 |
. . . . . . 7
⊢
(∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))) |
35 | 28, 32, 34 | 3bitr2ri 288 |
. . . . . 6
⊢ (({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})) ↔ ∃𝑤 𝐴 = {𝑤}) |
36 | 25, 35 | sylib 207 |
. . . . 5
⊢
(∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) → ∃𝑤 𝐴 = {𝑤}) |
37 | | eqid 2610 |
. . . . . 6
⊢ {𝐴, 𝐵} = {𝐴, 𝐵} |
38 | | prex 4836 |
. . . . . . 7
⊢ {𝐴, 𝐵} ∈ V |
39 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑧 = {𝐴, 𝐵} → (𝑧 = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴, 𝐵})) |
40 | | eqeq1 2614 |
. . . . . . . . 9
⊢ (𝑧 = {𝐴, 𝐵} → (𝑧 = 〈𝑥, 𝑦〉 ↔ {𝐴, 𝐵} = 〈𝑥, 𝑦〉)) |
41 | 40 | 2exbidv 1839 |
. . . . . . . 8
⊢ (𝑧 = {𝐴, 𝐵} → (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ↔ ∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉)) |
42 | 39, 41 | imbi12d 333 |
. . . . . . 7
⊢ (𝑧 = {𝐴, 𝐵} → ((𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ↔ ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉))) |
43 | 38, 42 | spcv 3272 |
. . . . . 6
⊢
(∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) → ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉)) |
44 | 37, 43 | mpi 20 |
. . . . 5
⊢
(∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) → ∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉) |
45 | | eqcom 2617 |
. . . . . . . . . 10
⊢ ({𝐴, 𝐵} = 〈𝑥, 𝑦〉 ↔ 〈𝑥, 𝑦〉 = {𝐴, 𝐵}) |
46 | 18, 19, 3, 4 | opeqpr 4893 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 = {𝐴, 𝐵} ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}))) |
47 | 45, 46 | bitri 263 |
. . . . . . . . 9
⊢ ({𝐴, 𝐵} = 〈𝑥, 𝑦〉 ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}))) |
48 | | idd 24 |
. . . . . . . . . 10
⊢ (𝐴 = {𝑤} → ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
49 | | eqtr2 2630 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → {𝑥, 𝑦} = {𝑤}) |
50 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑤 ∈ V |
51 | 18, 19, 50 | preqsn 4331 |
. . . . . . . . . . . . . . 15
⊢ ({𝑥, 𝑦} = {𝑤} ↔ (𝑥 = 𝑦 ∧ 𝑦 = 𝑤)) |
52 | 51 | simplbi 475 |
. . . . . . . . . . . . . 14
⊢ ({𝑥, 𝑦} = {𝑤} → 𝑥 = 𝑦) |
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → 𝑥 = 𝑦) |
54 | | dfsn2 4138 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑥} = {𝑥, 𝑥} |
55 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → {𝑥, 𝑥} = {𝑥, 𝑦}) |
56 | 54, 55 | syl5req 2657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → {𝑥, 𝑦} = {𝑥}) |
57 | 56 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} ↔ 𝐴 = {𝑥})) |
58 | 54, 55 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑥, 𝑦}) |
59 | 58 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐵 = {𝑥} ↔ 𝐵 = {𝑥, 𝑦})) |
60 | 57, 59 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) ↔ (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
61 | 60 | biimpd 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
62 | 61 | expd 451 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))) |
63 | 62 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = {𝑥, 𝑦} → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))) |
65 | 53, 64 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
66 | 65 | expcom 450 |
. . . . . . . . . . 11
⊢ (𝐴 = {𝑤} → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))) |
67 | 66 | impd 446 |
. . . . . . . . . 10
⊢ (𝐴 = {𝑤} → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
68 | 48, 67 | jaod 394 |
. . . . . . . . 9
⊢ (𝐴 = {𝑤} → (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
69 | 47, 68 | syl5bi 231 |
. . . . . . . 8
⊢ (𝐴 = {𝑤} → ({𝐴, 𝐵} = 〈𝑥, 𝑦〉 → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
70 | 69 | 2eximdv 1835 |
. . . . . . 7
⊢ (𝐴 = {𝑤} → (∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉 → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
71 | 70 | exlimiv 1845 |
. . . . . 6
⊢
(∃𝑤 𝐴 = {𝑤} → (∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉 → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
72 | 71 | imp 444 |
. . . . 5
⊢
((∃𝑤 𝐴 = {𝑤} ∧ ∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉) → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) |
73 | 36, 44, 72 | syl2an 493 |
. . . 4
⊢
((∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉)) → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) |
74 | 13, 73 | sylbi 206 |
. . 3
⊢
(〈𝐴, 𝐵〉 ⊆ (V × V)
→ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) |
75 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = {𝐴}) |
76 | | equid 1926 |
. . . . . . . . . . . . . 14
⊢ 𝑥 = 𝑥 |
77 | 76 | jctl 562 |
. . . . . . . . . . . . 13
⊢ (𝐴 = {𝑥} → (𝑥 = 𝑥 ∧ 𝐴 = {𝑥})) |
78 | 18, 18, 3 | opeqsn 4892 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑥〉 = {𝐴} ↔ (𝑥 = 𝑥 ∧ 𝐴 = {𝑥})) |
79 | 77, 78 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (𝐴 = {𝑥} → 〈𝑥, 𝑥〉 = {𝐴}) |
80 | 79 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 〈𝑥, 𝑥〉 = {𝐴}) |
81 | 75, 80 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = 〈𝑥, 𝑥〉) |
82 | | opeq12 4342 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑥) → 〈𝑤, 𝑣〉 = 〈𝑥, 𝑥〉) |
83 | 82 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑥) → (𝑧 = 〈𝑤, 𝑣〉 ↔ 𝑧 = 〈𝑥, 𝑥〉)) |
84 | 18, 18, 83 | spc2ev 3274 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑥〉 → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
85 | 81, 84 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
86 | 85 | adantlr 747 |
. . . . . . . 8
⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴}) → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
87 | | preq12 4214 |
. . . . . . . . . . . 12
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → {𝐴, 𝐵} = {{𝑥}, {𝑥, 𝑦}}) |
88 | 87 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 = {𝐴, 𝐵} ↔ 𝑧 = {{𝑥}, {𝑥, 𝑦}})) |
89 | 88 | biimpa 500 |
. . . . . . . . . 10
⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = {{𝑥}, {𝑥, 𝑦}}) |
90 | 18, 19 | dfop 4339 |
. . . . . . . . . 10
⊢
〈𝑥, 𝑦〉 = {{𝑥}, {𝑥, 𝑦}} |
91 | 89, 90 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = 〈𝑥, 𝑦〉) |
92 | | opeq12 4342 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → 〈𝑤, 𝑣〉 = 〈𝑥, 𝑦〉) |
93 | 92 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑧 = 〈𝑤, 𝑣〉 ↔ 𝑧 = 〈𝑥, 𝑦〉)) |
94 | 18, 19, 93 | spc2ev 3274 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
95 | 91, 94 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
96 | 86, 95 | jaodan 822 |
. . . . . . 7
⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵})) → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
97 | 96 | ex 449 |
. . . . . 6
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉)) |
98 | | elvv 5100 |
. . . . . 6
⊢ (𝑧 ∈ (V × V) ↔
∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
99 | 97, 5, 98 | 3imtr4g 284 |
. . . . 5
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V))) |
100 | 99 | ssrdv 3574 |
. . . 4
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → 〈𝐴, 𝐵〉 ⊆ (V ×
V)) |
101 | 100 | exlimivv 1847 |
. . 3
⊢
(∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → 〈𝐴, 𝐵〉 ⊆ (V ×
V)) |
102 | 74, 101 | impbii 198 |
. 2
⊢
(〈𝐴, 𝐵〉 ⊆ (V × V)
↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) |
103 | 1, 102 | bitri 263 |
1
⊢ (Rel
〈𝐴, 𝐵〉 ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) |