Step | Hyp | Ref
| Expression |
1 | | eluni 4848 |
. . . 4
⊢ (𝑥 ∈ ∪ 𝐴
↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) |
2 | | eluni 4848 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝐵
↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) |
3 | 2 | notbii 320 |
. . . 4
⊢ (¬
𝑥 ∈ ∪ 𝐵
↔ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) |
4 | | alinexa 1849 |
. . . . . 6
⊢
(∀𝑦(𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵) ↔ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) |
5 | | nfa1 2152 |
. . . . . . 7
⊢
Ⅎ𝑦∀𝑦(𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵) |
6 | | sp 2180 |
. . . . . . . . . 10
⊢
(∀𝑦(𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵)) |
7 | 6 | adantrd 492 |
. . . . . . . . 9
⊢
(∀𝑦(𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦 ∈ 𝐵)) |
8 | 7 | ancld 551 |
. . . . . . . 8
⊢
(∀𝑦(𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ∈ 𝐵))) |
9 | | anass 469 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))) |
10 | 8, 9 | syl6ib 250 |
. . . . . . 7
⊢
(∀𝑦(𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)))) |
11 | 5, 10 | eximd 2213 |
. . . . . 6
⊢
(∀𝑦(𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵) → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)))) |
12 | 4, 11 | sylbir 234 |
. . . . 5
⊢ (¬
∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)))) |
13 | 12 | impcom 408 |
. . . 4
⊢
((∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∧ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) → ∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))) |
14 | 1, 3, 13 | syl2anb 598 |
. . 3
⊢ ((𝑥 ∈ ∪ 𝐴
∧ ¬ 𝑥 ∈ ∪ 𝐵)
→ ∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))) |
15 | | eldif 3902 |
. . 3
⊢ (𝑥 ∈ (∪ 𝐴
∖ ∪ 𝐵) ↔ (𝑥 ∈ ∪ 𝐴 ∧ ¬ 𝑥 ∈ ∪ 𝐵)) |
16 | | eluni 4848 |
. . . 4
⊢ (𝑥 ∈ ∪ (𝐴
∖ 𝐵) ↔
∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∖ 𝐵))) |
17 | | eldif 3902 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴 ∖ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)) |
18 | 17 | anbi2i 623 |
. . . . 5
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∖ 𝐵)) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))) |
19 | 18 | exbii 1854 |
. . . 4
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∖ 𝐵)) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))) |
20 | 16, 19 | bitri 274 |
. . 3
⊢ (𝑥 ∈ ∪ (𝐴
∖ 𝐵) ↔
∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))) |
21 | 14, 15, 20 | 3imtr4i 292 |
. 2
⊢ (𝑥 ∈ (∪ 𝐴
∖ ∪ 𝐵) → 𝑥 ∈ ∪ (𝐴 ∖ 𝐵)) |
22 | 21 | ssriv 3930 |
1
⊢ (∪ 𝐴
∖ ∪ 𝐵) ⊆ ∪
(𝐴 ∖ 𝐵) |