Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > undif2 | Structured version Visualization version GIF version |
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3992). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.) |
Ref | Expression |
---|---|
undif2 | ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uncom 3719 | . 2 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∪ 𝐴) | |
2 | undif1 3995 | . 2 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴) | |
3 | uncom 3719 | . 2 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) | |
4 | 1, 2, 3 | 3eqtri 2636 | 1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∖ cdif 3537 ∪ cun 3538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 |
This theorem is referenced by: undif 4001 dfif5 4052 funiunfv 6410 difex2 6863 undom 7933 domss2 8004 sucdom2 8041 unfi 8112 marypha1lem 8222 kmlem11 8865 hashun2 13033 hashun3 13034 cvgcmpce 14391 dprd2da 18264 dpjcntz 18274 dpjdisj 18275 dpjlsm 18276 dpjidcl 18280 ablfac1eu 18295 dfcon2 21032 2ndcdisj2 21070 fixufil 21536 fin1aufil 21546 xrge0gsumle 22444 unmbl 23112 volsup 23131 mbfss 23219 itg2cnlem2 23335 iblss2 23378 amgm 24517 wilthlem2 24595 ftalem3 24601 rpvmasum2 25001 esumpad 29444 imadifss 32554 elrfi 36275 meaunle 39357 |
Copyright terms: Public domain | W3C validator |