Step | Hyp | Ref
| Expression |
1 | | elin 3758 |
. . . 4
⊢ (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ (𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣 ∈ 𝑦)) |
2 | | elxp 5055 |
. . . . . 6
⊢ (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑡∃𝑔(𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤))) |
3 | | excom 2029 |
. . . . . 6
⊢
(∃𝑡∃𝑔(𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤)) ↔ ∃𝑔∃𝑡(𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤))) |
4 | 2, 3 | bitri 263 |
. . . . 5
⊢ (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑔∃𝑡(𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤))) |
5 | 4 | anbi1i 727 |
. . . 4
⊢ ((𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣 ∈ 𝑦) ↔ (∃𝑔∃𝑡(𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤)) ∧ 𝑣 ∈ 𝑦)) |
6 | | 19.41vv 1902 |
. . . . 5
⊢
(∃𝑔∃𝑡((𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤)) ∧ 𝑣 ∈ 𝑦) ↔ (∃𝑔∃𝑡(𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤)) ∧ 𝑣 ∈ 𝑦)) |
7 | | an32 835 |
. . . . . . . . 9
⊢ (((𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤)) ∧ 𝑣 ∈ 𝑦) ↔ ((𝑣 = 〈𝑡, 𝑔〉 ∧ 𝑣 ∈ 𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤))) |
8 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑣 = 〈𝑡, 𝑔〉 → (𝑣 ∈ 𝑦 ↔ 〈𝑡, 𝑔〉 ∈ 𝑦)) |
9 | 8 | pm5.32i 667 |
. . . . . . . . . 10
⊢ ((𝑣 = 〈𝑡, 𝑔〉 ∧ 𝑣 ∈ 𝑦) ↔ (𝑣 = 〈𝑡, 𝑔〉 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦)) |
10 | | velsn 4141 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ {𝑤} ↔ 𝑡 = 𝑤) |
11 | 10 | anbi1i 727 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑤)) |
12 | 9, 11 | anbi12i 729 |
. . . . . . . . 9
⊢ (((𝑣 = 〈𝑡, 𝑔〉 ∧ 𝑣 ∈ 𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤)) ↔ ((𝑣 = 〈𝑡, 𝑔〉 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦) ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑤))) |
13 | | an4 861 |
. . . . . . . . . 10
⊢ (((𝑣 = 〈𝑡, 𝑔〉 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦) ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑤)) ↔ ((𝑣 = 〈𝑡, 𝑔〉 ∧ 𝑡 = 𝑤) ∧ (〈𝑡, 𝑔〉 ∈ 𝑦 ∧ 𝑔 ∈ 𝑤))) |
14 | | ancom 465 |
. . . . . . . . . . 11
⊢ ((𝑣 = 〈𝑡, 𝑔〉 ∧ 𝑡 = 𝑤) ↔ (𝑡 = 𝑤 ∧ 𝑣 = 〈𝑡, 𝑔〉)) |
15 | | ancom 465 |
. . . . . . . . . . 11
⊢
((〈𝑡, 𝑔〉 ∈ 𝑦 ∧ 𝑔 ∈ 𝑤) ↔ (𝑔 ∈ 𝑤 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦)) |
16 | 14, 15 | anbi12i 729 |
. . . . . . . . . 10
⊢ (((𝑣 = 〈𝑡, 𝑔〉 ∧ 𝑡 = 𝑤) ∧ (〈𝑡, 𝑔〉 ∈ 𝑦 ∧ 𝑔 ∈ 𝑤)) ↔ ((𝑡 = 𝑤 ∧ 𝑣 = 〈𝑡, 𝑔〉) ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦))) |
17 | | anass 679 |
. . . . . . . . . 10
⊢ (((𝑡 = 𝑤 ∧ 𝑣 = 〈𝑡, 𝑔〉) ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦)))) |
18 | 13, 16, 17 | 3bitri 285 |
. . . . . . . . 9
⊢ (((𝑣 = 〈𝑡, 𝑔〉 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦) ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑤)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦)))) |
19 | 7, 12, 18 | 3bitri 285 |
. . . . . . . 8
⊢ (((𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤)) ∧ 𝑣 ∈ 𝑦) ↔ (𝑡 = 𝑤 ∧ (𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦)))) |
20 | 19 | exbii 1764 |
. . . . . . 7
⊢
(∃𝑡((𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤)) ∧ 𝑣 ∈ 𝑦) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦)))) |
21 | | vex 3176 |
. . . . . . . 8
⊢ 𝑤 ∈ V |
22 | | opeq1 4340 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑤 → 〈𝑡, 𝑔〉 = 〈𝑤, 𝑔〉) |
23 | 22 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑡 = 𝑤 → (𝑣 = 〈𝑡, 𝑔〉 ↔ 𝑣 = 〈𝑤, 𝑔〉)) |
24 | 22 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑤 → (〈𝑡, 𝑔〉 ∈ 𝑦 ↔ 〈𝑤, 𝑔〉 ∈ 𝑦)) |
25 | 24 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑡 = 𝑤 → ((𝑔 ∈ 𝑤 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦) ↔ (𝑔 ∈ 𝑤 ∧ 〈𝑤, 𝑔〉 ∈ 𝑦))) |
26 | 23, 25 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → ((𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦)) ↔ (𝑣 = 〈𝑤, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑤, 𝑔〉 ∈ 𝑦)))) |
27 | 21, 26 | ceqsexv 3215 |
. . . . . . 7
⊢
(∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑡, 𝑔〉 ∈ 𝑦))) ↔ (𝑣 = 〈𝑤, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑤, 𝑔〉 ∈ 𝑦))) |
28 | 20, 27 | bitri 263 |
. . . . . 6
⊢
(∃𝑡((𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤)) ∧ 𝑣 ∈ 𝑦) ↔ (𝑣 = 〈𝑤, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑤, 𝑔〉 ∈ 𝑦))) |
29 | 28 | exbii 1764 |
. . . . 5
⊢
(∃𝑔∃𝑡((𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤)) ∧ 𝑣 ∈ 𝑦) ↔ ∃𝑔(𝑣 = 〈𝑤, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑤, 𝑔〉 ∈ 𝑦))) |
30 | 6, 29 | bitr3i 265 |
. . . 4
⊢
((∃𝑔∃𝑡(𝑣 = 〈𝑡, 𝑔〉 ∧ (𝑡 ∈ {𝑤} ∧ 𝑔 ∈ 𝑤)) ∧ 𝑣 ∈ 𝑦) ↔ ∃𝑔(𝑣 = 〈𝑤, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑤, 𝑔〉 ∈ 𝑦))) |
31 | 1, 5, 30 | 3bitri 285 |
. . 3
⊢ (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃𝑔(𝑣 = 〈𝑤, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑤, 𝑔〉 ∈ 𝑦))) |
32 | 31 | eubii 2480 |
. 2
⊢
(∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑣∃𝑔(𝑣 = 〈𝑤, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑤, 𝑔〉 ∈ 𝑦))) |
33 | 21 | euop2 4899 |
. 2
⊢
(∃!𝑣∃𝑔(𝑣 = 〈𝑤, 𝑔〉 ∧ (𝑔 ∈ 𝑤 ∧ 〈𝑤, 𝑔〉 ∈ 𝑦)) ↔ ∃!𝑔(𝑔 ∈ 𝑤 ∧ 〈𝑤, 𝑔〉 ∈ 𝑦)) |
34 | 32, 33 | bitri 263 |
1
⊢
(∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑔(𝑔 ∈ 𝑤 ∧ 〈𝑤, 𝑔〉 ∈ 𝑦)) |