Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . 4
⊢ (𝑤 = ∅ → 𝑤 = ∅) |
2 | | difeq2 3215 |
. . . 4
⊢ (𝑤 = ∅ → (𝐴 ∖ 𝑤) = (𝐴 ∖ ∅)) |
3 | 1, 2 | uneq12d 3258 |
. . 3
⊢ (𝑤 = ∅ → (𝑤 ∪ (𝐴 ∖ 𝑤)) = (∅ ∪ (𝐴 ∖ ∅))) |
4 | 3 | eqeq2d 2166 |
. 2
⊢ (𝑤 = ∅ → (𝐴 = (𝑤 ∪ (𝐴 ∖ 𝑤)) ↔ 𝐴 = (∅ ∪ (𝐴 ∖ ∅)))) |
5 | | id 19 |
. . . 4
⊢ (𝑤 = 𝑣 → 𝑤 = 𝑣) |
6 | | difeq2 3215 |
. . . 4
⊢ (𝑤 = 𝑣 → (𝐴 ∖ 𝑤) = (𝐴 ∖ 𝑣)) |
7 | 5, 6 | uneq12d 3258 |
. . 3
⊢ (𝑤 = 𝑣 → (𝑤 ∪ (𝐴 ∖ 𝑤)) = (𝑣 ∪ (𝐴 ∖ 𝑣))) |
8 | 7 | eqeq2d 2166 |
. 2
⊢ (𝑤 = 𝑣 → (𝐴 = (𝑤 ∪ (𝐴 ∖ 𝑤)) ↔ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣)))) |
9 | | id 19 |
. . . 4
⊢ (𝑤 = (𝑣 ∪ {𝑧}) → 𝑤 = (𝑣 ∪ {𝑧})) |
10 | | difeq2 3215 |
. . . 4
⊢ (𝑤 = (𝑣 ∪ {𝑧}) → (𝐴 ∖ 𝑤) = (𝐴 ∖ (𝑣 ∪ {𝑧}))) |
11 | 9, 10 | uneq12d 3258 |
. . 3
⊢ (𝑤 = (𝑣 ∪ {𝑧}) → (𝑤 ∪ (𝐴 ∖ 𝑤)) = ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧})))) |
12 | 11 | eqeq2d 2166 |
. 2
⊢ (𝑤 = (𝑣 ∪ {𝑧}) → (𝐴 = (𝑤 ∪ (𝐴 ∖ 𝑤)) ↔ 𝐴 = ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧}))))) |
13 | | id 19 |
. . . 4
⊢ (𝑤 = 𝐵 → 𝑤 = 𝐵) |
14 | | difeq2 3215 |
. . . 4
⊢ (𝑤 = 𝐵 → (𝐴 ∖ 𝑤) = (𝐴 ∖ 𝐵)) |
15 | 13, 14 | uneq12d 3258 |
. . 3
⊢ (𝑤 = 𝐵 → (𝑤 ∪ (𝐴 ∖ 𝑤)) = (𝐵 ∪ (𝐴 ∖ 𝐵))) |
16 | 15 | eqeq2d 2166 |
. 2
⊢ (𝑤 = 𝐵 → (𝐴 = (𝑤 ∪ (𝐴 ∖ 𝑤)) ↔ 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))) |
17 | | un0 3423 |
. . . 4
⊢ ((𝐴 ∖ ∅) ∪ ∅)
= (𝐴 ∖
∅) |
18 | | uncom 3247 |
. . . 4
⊢ ((𝐴 ∖ ∅) ∪ ∅)
= (∅ ∪ (𝐴 ∖
∅)) |
19 | | dif0 3460 |
. . . 4
⊢ (𝐴 ∖ ∅) = 𝐴 |
20 | 17, 18, 19 | 3eqtr3ri 2184 |
. . 3
⊢ 𝐴 = (∅ ∪ (𝐴 ∖
∅)) |
21 | 20 | a1i 9 |
. 2
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (∅ ∪ (𝐴 ∖ ∅))) |
22 | | difundi 3355 |
. . . . . . 7
⊢ (𝐴 ∖ (𝑣 ∪ {𝑧})) = ((𝐴 ∖ 𝑣) ∩ (𝐴 ∖ {𝑧})) |
23 | 22 | uneq2i 3254 |
. . . . . 6
⊢ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧}))) = ((𝑣 ∪ {𝑧}) ∪ ((𝐴 ∖ 𝑣) ∩ (𝐴 ∖ {𝑧}))) |
24 | | undi 3351 |
. . . . . 6
⊢ ((𝑣 ∪ {𝑧}) ∪ ((𝐴 ∖ 𝑣) ∩ (𝐴 ∖ {𝑧}))) = (((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) ∩ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧}))) |
25 | 23, 24 | eqtri 2175 |
. . . . 5
⊢ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧}))) = (((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) ∩ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧}))) |
26 | | uncom 3247 |
. . . . . . . . 9
⊢ (𝑣 ∪ {𝑧}) = ({𝑧} ∪ 𝑣) |
27 | 26 | uneq1i 3253 |
. . . . . . . 8
⊢ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) = (({𝑧} ∪ 𝑣) ∪ (𝐴 ∖ 𝑣)) |
28 | | unass 3260 |
. . . . . . . 8
⊢ (({𝑧} ∪ 𝑣) ∪ (𝐴 ∖ 𝑣)) = ({𝑧} ∪ (𝑣 ∪ (𝐴 ∖ 𝑣))) |
29 | 27, 28 | eqtri 2175 |
. . . . . . 7
⊢ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) = ({𝑧} ∪ (𝑣 ∪ (𝐴 ∖ 𝑣))) |
30 | | simp3 984 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐴) |
31 | 30 | ad3antrrr 484 |
. . . . . . . . . . 11
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝐵 ⊆ 𝐴) |
32 | | simplrr 526 |
. . . . . . . . . . . 12
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝑧 ∈ (𝐵 ∖ 𝑣)) |
33 | 32 | eldifad 3109 |
. . . . . . . . . . 11
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝑧 ∈ 𝐵) |
34 | 31, 33 | sseldd 3125 |
. . . . . . . . . 10
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝑧 ∈ 𝐴) |
35 | 34 | snssd 3697 |
. . . . . . . . 9
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → {𝑧} ⊆ 𝐴) |
36 | | ssequn1 3273 |
. . . . . . . . 9
⊢ ({𝑧} ⊆ 𝐴 ↔ ({𝑧} ∪ 𝐴) = 𝐴) |
37 | 35, 36 | sylib 121 |
. . . . . . . 8
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ({𝑧} ∪ 𝐴) = 𝐴) |
38 | | simpr 109 |
. . . . . . . . 9
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) |
39 | 38 | uneq2d 3257 |
. . . . . . . 8
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ({𝑧} ∪ 𝐴) = ({𝑧} ∪ (𝑣 ∪ (𝐴 ∖ 𝑣)))) |
40 | 37, 39 | eqtr3d 2189 |
. . . . . . 7
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝐴 = ({𝑧} ∪ (𝑣 ∪ (𝐴 ∖ 𝑣)))) |
41 | 29, 40 | eqtr4id 2206 |
. . . . . 6
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) = 𝐴) |
42 | | unass 3260 |
. . . . . . . 8
⊢ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧})) = (𝑣 ∪ ({𝑧} ∪ (𝐴 ∖ {𝑧}))) |
43 | | uncom 3247 |
. . . . . . . . . 10
⊢ ({𝑧} ∪ (𝐴 ∖ {𝑧})) = ((𝐴 ∖ {𝑧}) ∪ {𝑧}) |
44 | | simp1 982 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) |
45 | 44 | ad3antrrr 484 |
. . . . . . . . . . 11
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) |
46 | | dcdifsnid 6440 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝑧 ∈ 𝐴) → ((𝐴 ∖ {𝑧}) ∪ {𝑧}) = 𝐴) |
47 | 45, 34, 46 | syl2anc 409 |
. . . . . . . . . 10
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ((𝐴 ∖ {𝑧}) ∪ {𝑧}) = 𝐴) |
48 | 43, 47 | syl5eq 2199 |
. . . . . . . . 9
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ({𝑧} ∪ (𝐴 ∖ {𝑧})) = 𝐴) |
49 | 48 | uneq2d 3257 |
. . . . . . . 8
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → (𝑣 ∪ ({𝑧} ∪ (𝐴 ∖ {𝑧}))) = (𝑣 ∪ 𝐴)) |
50 | 42, 49 | syl5eq 2199 |
. . . . . . 7
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧})) = (𝑣 ∪ 𝐴)) |
51 | | simplrl 525 |
. . . . . . . . 9
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝑣 ⊆ 𝐵) |
52 | 51, 31 | sstrd 3134 |
. . . . . . . 8
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝑣 ⊆ 𝐴) |
53 | | ssequn1 3273 |
. . . . . . . 8
⊢ (𝑣 ⊆ 𝐴 ↔ (𝑣 ∪ 𝐴) = 𝐴) |
54 | 52, 53 | sylib 121 |
. . . . . . 7
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → (𝑣 ∪ 𝐴) = 𝐴) |
55 | 50, 54 | eqtrd 2187 |
. . . . . 6
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧})) = 𝐴) |
56 | 41, 55 | ineq12d 3305 |
. . . . 5
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → (((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) ∩ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧}))) = (𝐴 ∩ 𝐴)) |
57 | 25, 56 | syl5eq 2199 |
. . . 4
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧}))) = (𝐴 ∩ 𝐴)) |
58 | | inidm 3312 |
. . . 4
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
59 | 57, 58 | eqtr2di 2204 |
. . 3
⊢
(((((∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝐴 = ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧})))) |
60 | 59 | ex 114 |
. 2
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) → (𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣)) → 𝐴 = ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧}))))) |
61 | | simp2 983 |
. 2
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) |
62 | 4, 8, 12, 16, 21, 60, 61 | findcard2sd 6826 |
1
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵))) |