Step | Hyp | Ref
| Expression |
1 | | eeanv 1913 |
. . . . 5
⊢ (∃w∃v(x = 〈y, w〉 ∧ x = 〈v, z〉) ↔ (∃w x = 〈y, w〉 ∧ ∃v x = 〈v, z〉)) |
2 | | vex 2862 |
. . . . . . . 8
⊢ z ∈
V |
3 | | vex 2862 |
. . . . . . . 8
⊢ y ∈
V |
4 | | opeq2 4579 |
. . . . . . . . . 10
⊢ (w = z →
〈y,
w〉 =
〈y,
z〉) |
5 | 4 | eqeq2d 2364 |
. . . . . . . . 9
⊢ (w = z →
(x = 〈y, w〉 ↔ x = 〈y, z〉)) |
6 | | opeq1 4578 |
. . . . . . . . . 10
⊢ (v = y →
〈v,
z〉 =
〈y,
z〉) |
7 | 6 | eqeq2d 2364 |
. . . . . . . . 9
⊢ (v = y →
(x = 〈v, z〉 ↔ x = 〈y, z〉)) |
8 | 5, 7 | bi2anan9 843 |
. . . . . . . 8
⊢ ((w = z ∧ v = y) → ((x =
〈y,
w〉 ∧ x = 〈v, z〉) ↔
(x = 〈y, z〉 ∧ x = 〈y, z〉))) |
9 | 2, 3, 8 | spc2ev 2947 |
. . . . . . 7
⊢ ((x = 〈y, z〉 ∧ x = 〈y, z〉) → ∃w∃v(x = 〈y, w〉 ∧ x = 〈v, z〉)) |
10 | 9 | anidms 626 |
. . . . . 6
⊢ (x = 〈y, z〉 → ∃w∃v(x = 〈y, w〉 ∧ x = 〈v, z〉)) |
11 | | simpl 443 |
. . . . . . . 8
⊢ ((x = 〈y, w〉 ∧ x = 〈v, z〉) → x =
〈y,
w〉) |
12 | | eqtr2 2371 |
. . . . . . . . 9
⊢ ((x = 〈y, w〉 ∧ x = 〈v, z〉) → 〈y, w〉 = 〈v, z〉) |
13 | | opth 4602 |
. . . . . . . . . 10
⊢ (〈y, w〉 = 〈v, z〉 ↔
(y = v
∧ w =
z)) |
14 | 4 | adantl 452 |
. . . . . . . . . 10
⊢ ((y = v ∧ w = z) → 〈y, w〉 = 〈y, z〉) |
15 | 13, 14 | sylbi 187 |
. . . . . . . . 9
⊢ (〈y, w〉 = 〈v, z〉 → 〈y, w〉 = 〈y, z〉) |
16 | 12, 15 | syl 15 |
. . . . . . . 8
⊢ ((x = 〈y, w〉 ∧ x = 〈v, z〉) → 〈y, w〉 = 〈y, z〉) |
17 | 11, 16 | eqtrd 2385 |
. . . . . . 7
⊢ ((x = 〈y, w〉 ∧ x = 〈v, z〉) → x =
〈y,
z〉) |
18 | 17 | exlimivv 1635 |
. . . . . 6
⊢ (∃w∃v(x = 〈y, w〉 ∧ x = 〈v, z〉) → x =
〈y,
z〉) |
19 | 10, 18 | impbii 180 |
. . . . 5
⊢ (x = 〈y, z〉 ↔ ∃w∃v(x = 〈y, w〉 ∧ x = 〈v, z〉)) |
20 | | brcnv 4892 |
. . . . . . 7
⊢ (y◡1st x ↔ x1st y) |
21 | 3 | br1st 4858 |
. . . . . . 7
⊢ (x1st y ↔ ∃w x = 〈y, w〉) |
22 | 20, 21 | bitri 240 |
. . . . . 6
⊢ (y◡1st x ↔ ∃w x = 〈y, w〉) |
23 | | brcnv 4892 |
. . . . . . 7
⊢ (z◡2nd x ↔ x2nd z) |
24 | 2 | br2nd 4859 |
. . . . . . 7
⊢ (x2nd z ↔ ∃v x = 〈v, z〉) |
25 | 23, 24 | bitri 240 |
. . . . . 6
⊢ (z◡2nd x ↔ ∃v x = 〈v, z〉) |
26 | 22, 25 | anbi12i 678 |
. . . . 5
⊢ ((y◡1st x ∧ z◡2nd x) ↔ (∃w x = 〈y, w〉 ∧ ∃v x = 〈v, z〉)) |
27 | 1, 19, 26 | 3bitr4i 268 |
. . . 4
⊢ (x = 〈y, z〉 ↔ (y◡1st x ∧ z◡2nd x)) |
28 | 27 | 2rexbii 2641 |
. . 3
⊢ (∃y ∈ A ∃z ∈ B x = 〈y, z〉 ↔ ∃y ∈ A ∃z ∈ B (y◡1st x ∧ z◡2nd x)) |
29 | | elxp2 4802 |
. . 3
⊢ (x ∈ (A × B)
↔ ∃y ∈ A ∃z ∈ B x = 〈y, z〉) |
30 | | elima 4754 |
. . . . 5
⊢ (x ∈ (◡1st “ A) ↔ ∃y ∈ A y◡1st x) |
31 | | elima 4754 |
. . . . 5
⊢ (x ∈ (◡2nd “ B) ↔ ∃z ∈ B z◡2nd x) |
32 | 30, 31 | anbi12i 678 |
. . . 4
⊢ ((x ∈ (◡1st “ A) ∧ x ∈ (◡2nd “ B)) ↔ (∃y ∈ A y◡1st x ∧ ∃z ∈ B z◡2nd x)) |
33 | | elin 3219 |
. . . 4
⊢ (x ∈ ((◡1st “ A) ∩ (◡2nd “ B)) ↔ (x
∈ (◡1st “ A) ∧ x ∈ (◡2nd “ B))) |
34 | | reeanv 2778 |
. . . 4
⊢ (∃y ∈ A ∃z ∈ B (y◡1st x ∧ z◡2nd x) ↔ (∃y ∈ A y◡1st x ∧ ∃z ∈ B z◡2nd x)) |
35 | 32, 33, 34 | 3bitr4i 268 |
. . 3
⊢ (x ∈ ((◡1st “ A) ∩ (◡2nd “ B)) ↔ ∃y ∈ A ∃z ∈ B (y◡1st x ∧ z◡2nd x)) |
36 | 28, 29, 35 | 3bitr4i 268 |
. 2
⊢ (x ∈ (A × B)
↔ x ∈ ((◡1st “ A) ∩ (◡2nd “ B))) |
37 | 36 | eqriv 2350 |
1
⊢ (A × B) =
((◡1st “ A) ∩ (◡2nd “ B)) |