Step | Hyp | Ref
| Expression |
1 | | ssel 2933 |
. . 3
⊢ (A ⊆ B
→ (〈x, y〉 ∈ A → 〈x, y〉 ∈ B)) |
2 | 1 | alrimivv 1752 |
. 2
⊢ (A ⊆ B
→ ∀x∀y(〈x,
y〉 ∈
A → 〈x, y〉 ∈ B)) |
3 | | eleq1 2097 |
. . . . . . . . . . 11
⊢ (z = 〈x,
y〉 → (z ∈ A ↔ 〈x, y〉 ∈ A)) |
4 | | eleq1 2097 |
. . . . . . . . . . 11
⊢ (z = 〈x,
y〉 → (z ∈ B ↔ 〈x, y〉 ∈ B)) |
5 | 3, 4 | imbi12d 223 |
. . . . . . . . . 10
⊢ (z = 〈x,
y〉 → ((z ∈ A → z ∈ B) ↔
(〈x, y〉 ∈ A → 〈x, y〉 ∈ B))) |
6 | 5 | biimprcd 149 |
. . . . . . . . 9
⊢
((〈x, y〉 ∈ A → 〈x, y〉 ∈ B) →
(z = 〈x, y〉
→ (z ∈ A →
z ∈
B))) |
7 | 6 | 2alimi 1342 |
. . . . . . . 8
⊢ (∀x∀y(〈x,
y〉 ∈
A → 〈x, y〉 ∈ B) →
∀x∀y(z = 〈x,
y〉 → (z ∈ A → z ∈ B))) |
8 | | 19.23vv 1761 |
. . . . . . . 8
⊢ (∀x∀y(z = 〈x,
y〉 → (z ∈ A → z ∈ B)) ↔
(∃x∃y z = 〈x,
y〉 → (z ∈ A → z ∈ B))) |
9 | 7, 8 | sylib 127 |
. . . . . . 7
⊢ (∀x∀y(〈x,
y〉 ∈
A → 〈x, y〉 ∈ B) →
(∃x∃y z = 〈x,
y〉 → (z ∈ A → z ∈ B))) |
10 | 9 | com23 72 |
. . . . . 6
⊢ (∀x∀y(〈x,
y〉 ∈
A → 〈x, y〉 ∈ B) →
(z ∈
A → (∃x∃y z = 〈x,
y〉 → z ∈ B))) |
11 | 10 | a2d 23 |
. . . . 5
⊢ (∀x∀y(〈x,
y〉 ∈
A → 〈x, y〉 ∈ B) →
((z ∈
A → ∃x∃y z = 〈x,
y〉) → (z ∈ A → z ∈ B))) |
12 | 11 | alimdv 1756 |
. . . 4
⊢ (∀x∀y(〈x,
y〉 ∈
A → 〈x, y〉 ∈ B) →
(∀z(z ∈ A →
∃x∃y z = 〈x,
y〉) → ∀z(z ∈ A → z ∈ B))) |
13 | | df-rel 4295 |
. . . . 5
⊢ (Rel
A ↔ A ⊆ (V × V)) |
14 | | dfss2 2928 |
. . . . 5
⊢ (A ⊆ (V × V) ↔ ∀z(z ∈ A → z ∈ (V × V))) |
15 | | elvv 4345 |
. . . . . . 7
⊢ (z ∈ (V × V)
↔ ∃x∃y z =
〈x, y〉) |
16 | 15 | imbi2i 215 |
. . . . . 6
⊢
((z ∈ A →
z ∈ (V
× V)) ↔ (z ∈ A →
∃x∃y z = 〈x,
y〉)) |
17 | 16 | albii 1356 |
. . . . 5
⊢ (∀z(z ∈ A → z ∈ (V × V)) ↔ ∀z(z ∈ A → ∃x∃y z = 〈x,
y〉)) |
18 | 13, 14, 17 | 3bitri 195 |
. . . 4
⊢ (Rel
A ↔ ∀z(z ∈ A → ∃x∃y z = 〈x,
y〉)) |
19 | | dfss2 2928 |
. . . 4
⊢ (A ⊆ B
↔ ∀z(z ∈ A →
z ∈
B)) |
20 | 12, 18, 19 | 3imtr4g 194 |
. . 3
⊢ (∀x∀y(〈x,
y〉 ∈
A → 〈x, y〉 ∈ B) →
(Rel A → A ⊆ B)) |
21 | 20 | com12 27 |
. 2
⊢ (Rel
A → (∀x∀y(〈x,
y〉 ∈
A → 〈x, y〉 ∈ B) →
A ⊆ B)) |
22 | 2, 21 | impbid2 131 |
1
⊢ (Rel
A → (A ⊆ B
↔ ∀x∀y(〈x,
y〉 ∈
A → 〈x, y〉 ∈ B))) |