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 2863 |
. . . . . . . 8
⊢ z ∈
V |
3 | | vex 2863 |
. . . . . . . 8
⊢ y ∈
V |
4 | | opeq2 4580 |
. . . . . . . . . 10
⊢ (w = z →
⟨y,
w⟩ =
⟨y,
z⟩) |
5 | 4 | eqeq2d 2364 |
. . . . . . . . 9
⊢ (w = z →
(x = ⟨y, w⟩ ↔ x = ⟨y, z⟩)) |
6 | | opeq1 4579 |
. . . . . . . . . 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 2948 |
. . . . . . 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 4603 |
. . . . . . . . . 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 4893 |
. . . . . . 7
⊢ (y◡1st x ↔ x1st y) |
21 | 3 | br1st 4859 |
. . . . . . 7
⊢ (x1st y ↔ ∃w x = ⟨y, w⟩) |
22 | 20, 21 | bitri 240 |
. . . . . 6
⊢ (y◡1st x ↔ ∃w x = ⟨y, w⟩) |
23 | | brcnv 4893 |
. . . . . . 7
⊢ (z◡2nd x ↔ x2nd z) |
24 | 2 | br2nd 4860 |
. . . . . . 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 2642 |
. . 3
⊢ (∃y ∈ A ∃z ∈ B x = ⟨y, z⟩ ↔ ∃y ∈ A ∃z ∈ B (y◡1st x ∧ z◡2nd x)) |
29 | | elxp2 4803 |
. . 3
⊢ (x ∈ (A × B)
↔ ∃y ∈ A ∃z ∈ B x = ⟨y, z⟩) |
30 | | elima 4755 |
. . . . 5
⊢ (x ∈ (◡1st “ A) ↔ ∃y ∈ A y◡1st x) |
31 | | elima 4755 |
. . . . 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 3220 |
. . . 4
⊢ (x ∈ ((◡1st “ A) ∩ (◡2nd “ B)) ↔ (x
∈ (◡1st “ A) ∧ x ∈ (◡2nd “ B))) |
34 | | reeanv 2779 |
. . . 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)) |