Step | Hyp | Ref
| Expression |
1 | | ssrel 4845 |
. . 3
⊢ (A ⊆ B ↔ ∀w∀z(⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B)) |
2 | | alcom 1737 |
. . 3
⊢ (∀w∀z(⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B) ↔
∀z∀w(⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B)) |
3 | 1, 2 | bitri 240 |
. 2
⊢ (A ⊆ B ↔ ∀z∀w(⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B)) |
4 | | vex 2863 |
. . . . . . . 8
⊢ w ∈
V |
5 | | opeqex 4622 |
. . . . . . . 8
⊢ (w ∈ V → ∃x∃y w = ⟨x, y⟩) |
6 | 4, 5 | ax-mp 5 |
. . . . . . 7
⊢ ∃x∃y w = ⟨x, y⟩ |
7 | 6 | a1bi 327 |
. . . . . 6
⊢ ((⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B) ↔
(∃x∃y w = ⟨x, y⟩ → (⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B))) |
8 | | 19.23vv 1892 |
. . . . . 6
⊢ (∀x∀y(w = ⟨x, y⟩ → (⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B)) ↔
(∃x∃y w = ⟨x, y⟩ → (⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B))) |
9 | 7, 8 | bitr4i 243 |
. . . . 5
⊢ ((⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B) ↔
∀x∀y(w = ⟨x, y⟩ → (⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B))) |
10 | 9 | albii 1566 |
. . . 4
⊢ (∀w(⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B) ↔
∀w∀x∀y(w = ⟨x, y⟩ → (⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B))) |
11 | | alrot3 1738 |
. . . 4
⊢ (∀w∀x∀y(w = ⟨x, y⟩ → (⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B)) ↔
∀x∀y∀w(w = ⟨x, y⟩ → (⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B))) |
12 | | vex 2863 |
. . . . . . 7
⊢ x ∈
V |
13 | | vex 2863 |
. . . . . . 7
⊢ y ∈
V |
14 | 12, 13 | opex 4589 |
. . . . . 6
⊢ ⟨x, y⟩ ∈ V |
15 | | opeq1 4579 |
. . . . . . . 8
⊢ (w = ⟨x, y⟩ → ⟨w, z⟩ = ⟨⟨x, y⟩, z⟩) |
16 | 15 | eleq1d 2419 |
. . . . . . 7
⊢ (w = ⟨x, y⟩ → (⟨w, z⟩ ∈ A ↔
⟨⟨x, y⟩, z⟩ ∈ A)) |
17 | 15 | eleq1d 2419 |
. . . . . . 7
⊢ (w = ⟨x, y⟩ → (⟨w, z⟩ ∈ B ↔
⟨⟨x, y⟩, z⟩ ∈ B)) |
18 | 16, 17 | imbi12d 311 |
. . . . . 6
⊢ (w = ⟨x, y⟩ → ((⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B) ↔
(⟨⟨x, y⟩, z⟩ ∈ A → ⟨⟨x, y⟩, z⟩ ∈ B))) |
19 | 14, 18 | ceqsalv 2886 |
. . . . 5
⊢ (∀w(w = ⟨x, y⟩ → (⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B)) ↔
(⟨⟨x, y⟩, z⟩ ∈ A → ⟨⟨x, y⟩, z⟩ ∈ B)) |
20 | 19 | 2albii 1567 |
. . . 4
⊢ (∀x∀y∀w(w = ⟨x, y⟩ → (⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B)) ↔
∀x∀y(⟨⟨x, y⟩, z⟩ ∈ A → ⟨⟨x, y⟩, z⟩ ∈ B)) |
21 | 10, 11, 20 | 3bitri 262 |
. . 3
⊢ (∀w(⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B) ↔
∀x∀y(⟨⟨x, y⟩, z⟩ ∈ A → ⟨⟨x, y⟩, z⟩ ∈ B)) |
22 | 21 | albii 1566 |
. 2
⊢ (∀z∀w(⟨w, z⟩ ∈ A →
⟨w,
z⟩ ∈ B) ↔
∀z∀x∀y(⟨⟨x, y⟩, z⟩ ∈ A → ⟨⟨x, y⟩, z⟩ ∈ B)) |
23 | | alrot3 1738 |
. 2
⊢ (∀z∀x∀y(⟨⟨x, y⟩, z⟩ ∈ A → ⟨⟨x, y⟩, z⟩ ∈ B) ↔
∀x∀y∀z(⟨⟨x, y⟩, z⟩ ∈ A → ⟨⟨x, y⟩, z⟩ ∈ B)) |
24 | 3, 22, 23 | 3bitri 262 |
1
⊢ (A ⊆ B ↔ ∀x∀y∀z(⟨⟨x, y⟩, z⟩ ∈ A → ⟨⟨x, y⟩, z⟩ ∈ B)) |