| Step | Hyp | Ref
| Expression |
| 1 | | eluni 4910 |
. . . . . 6
⊢ (𝑦 ∈ ∪ 𝐴
↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) |
| 2 | 1 | imbi1i 349 |
. . . . 5
⊢ ((𝑦 ∈ ∪ 𝐴
→ 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
| 3 | | 19.23v 1942 |
. . . . 5
⊢
(∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
| 4 | 2, 3 | bitr4i 278 |
. . . 4
⊢ ((𝑦 ∈ ∪ 𝐴
→ 𝑦 ∈ 𝐵) ↔ ∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
| 5 | 4 | albii 1819 |
. . 3
⊢
(∀𝑦(𝑦 ∈ ∪ 𝐴
→ 𝑦 ∈ 𝐵) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
| 6 | | elequ1 2115 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
| 7 | 6 | anbi1d 631 |
. . . . . 6
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))) |
| 8 | | eleq1w 2824 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)) |
| 9 | 7, 8 | imbi12d 344 |
. . . . 5
⊢ (𝑦 = 𝑧 → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐵))) |
| 10 | | elequ2 2123 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)) |
| 11 | | eleq1w 2824 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
| 12 | 10, 11 | anbi12d 632 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴))) |
| 13 | 12 | imbi1d 341 |
. . . . 5
⊢ (𝑥 = 𝑧 → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝐵))) |
| 14 | 9, 13 | alcomw 2044 |
. . . 4
⊢
(∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
| 15 | | 19.21v 1939 |
. . . . . 6
⊢
(∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
| 16 | | impexp 450 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵))) |
| 17 | | bi2.04 387 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
| 18 | 16, 17 | bitri 275 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
| 19 | 18 | albii 1819 |
. . . . . 6
⊢
(∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
| 20 | | df-ss 3968 |
. . . . . . 7
⊢ (𝑥 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) |
| 21 | 20 | imbi2i 336 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
| 22 | 15, 19, 21 | 3bitr4i 303 |
. . . . 5
⊢
(∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
| 23 | 22 | albii 1819 |
. . . 4
⊢
(∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
| 24 | 14, 23 | bitri 275 |
. . 3
⊢
(∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
| 25 | 5, 24 | bitri 275 |
. 2
⊢
(∀𝑦(𝑦 ∈ ∪ 𝐴
→ 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
| 26 | | df-ss 3968 |
. 2
⊢ (∪ 𝐴
⊆ 𝐵 ↔
∀𝑦(𝑦 ∈ ∪ 𝐴
→ 𝑦 ∈ 𝐵)) |
| 27 | | df-ral 3062 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝑥 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
| 28 | 25, 26, 27 | 3bitr4i 303 |
1
⊢ (∪ 𝐴
⊆ 𝐵 ↔
∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |