Step | Hyp | Ref
| Expression |
1 | | n0i 3399 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑦 → ¬ 𝑦 = ∅) |
2 | 1 | pm4.71i 389 |
. . . . . 6
⊢ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ ¬ 𝑦 = ∅)) |
3 | 2 | anbi1i 454 |
. . . . 5
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ↔ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑦 = ∅) ∧ 𝑦 ∈ 𝐴)) |
4 | | an32 552 |
. . . . 5
⊢ (((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 = ∅) ↔ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑦 = ∅) ∧ 𝑦 ∈ 𝐴)) |
5 | | anass 399 |
. . . . 5
⊢ (((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 = ∅) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = ∅))) |
6 | 3, 4, 5 | 3bitr2ri 208 |
. . . 4
⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = ∅)) ↔ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) |
7 | 6 | exbii 1585 |
. . 3
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = ∅)) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) |
8 | | eluni 3775 |
. . . 4
⊢ (𝑥 ∈ ∪ (𝐴
∖ {∅}) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∖ {∅}))) |
9 | | eldif 3111 |
. . . . . . 7
⊢ (𝑦 ∈ (𝐴 ∖ {∅}) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ {∅})) |
10 | | velsn 3577 |
. . . . . . . . 9
⊢ (𝑦 ∈ {∅} ↔ 𝑦 = ∅) |
11 | 10 | notbii 658 |
. . . . . . . 8
⊢ (¬
𝑦 ∈ {∅} ↔
¬ 𝑦 =
∅) |
12 | 11 | anbi2i 453 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ {∅}) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = ∅)) |
13 | 9, 12 | bitri 183 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴 ∖ {∅}) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = ∅)) |
14 | 13 | anbi2i 453 |
. . . . 5
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∖ {∅})) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = ∅))) |
15 | 14 | exbii 1585 |
. . . 4
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∖ {∅})) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = ∅))) |
16 | 8, 15 | bitri 183 |
. . 3
⊢ (𝑥 ∈ ∪ (𝐴
∖ {∅}) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = ∅))) |
17 | | eluni 3775 |
. . 3
⊢ (𝑥 ∈ ∪ 𝐴
↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) |
18 | 7, 16, 17 | 3bitr4i 211 |
. 2
⊢ (𝑥 ∈ ∪ (𝐴
∖ {∅}) ↔ 𝑥
∈ ∪ 𝐴) |
19 | 18 | eqriv 2154 |
1
⊢ ∪ (𝐴
∖ {∅}) = ∪ 𝐴 |