Step | Hyp | Ref
| Expression |
1 | | eluni 4912 |
. . . . . 6
⊢ (𝑦 ∈ ∪ 𝐴
↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) |
2 | 1 | imbi1i 350 |
. . . . 5
⊢ ((𝑦 ∈ ∪ 𝐴
→ 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
3 | | 19.23v 1946 |
. . . . 5
⊢
(∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
4 | 2, 3 | bitr4i 278 |
. . . 4
⊢ ((𝑦 ∈ ∪ 𝐴
→ 𝑦 ∈ 𝐵) ↔ ∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
5 | 4 | albii 1822 |
. . 3
⊢
(∀𝑦(𝑦 ∈ ∪ 𝐴
→ 𝑦 ∈ 𝐵) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
6 | | elequ1 2114 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
7 | 6 | anbi1d 631 |
. . . . . 6
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))) |
8 | | eleq1w 2817 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)) |
9 | 7, 8 | imbi12d 345 |
. . . . 5
⊢ (𝑦 = 𝑧 → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐵))) |
10 | | elequ2 2122 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)) |
11 | | eleq1w 2817 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
12 | 10, 11 | anbi12d 632 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴))) |
13 | 12 | imbi1d 342 |
. . . . 5
⊢ (𝑥 = 𝑧 → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝐵))) |
14 | 9, 13 | alcomw 2048 |
. . . 4
⊢
(∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
15 | | 19.21v 1943 |
. . . . . 6
⊢
(∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
16 | | impexp 452 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵))) |
17 | | bi2.04 389 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
18 | 16, 17 | bitri 275 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
19 | 18 | albii 1822 |
. . . . . 6
⊢
(∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
20 | | dfss2 3969 |
. . . . . . 7
⊢ (𝑥 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) |
21 | 20 | imbi2i 336 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
22 | 15, 19, 21 | 3bitr4i 303 |
. . . . 5
⊢
(∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
23 | 22 | albii 1822 |
. . . 4
⊢
(∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
24 | 14, 23 | bitri 275 |
. . 3
⊢
(∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
25 | 5, 24 | bitri 275 |
. 2
⊢
(∀𝑦(𝑦 ∈ ∪ 𝐴
→ 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
26 | | dfss2 3969 |
. 2
⊢ (∪ 𝐴
⊆ 𝐵 ↔
∀𝑦(𝑦 ∈ ∪ 𝐴
→ 𝑦 ∈ 𝐵)) |
27 | | df-ral 3063 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝑥 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
28 | 25, 26, 27 | 3bitr4i 303 |
1
⊢ (∪ 𝐴
⊆ 𝐵 ↔
∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |