| 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 4431). 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 4117 | . 2 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∪ 𝐴) | |
| 2 | undif1 4435 | . 2 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴) | |
| 3 | uncom 4117 | . 2 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) | |
| 4 | 1, 2, 3 | 3eqtri 2756 | 1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∖ cdif 3908 ∪ cun 3909 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2701 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-rab 3403 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 |
| This theorem is referenced by: undif 4441 dfif5 4501 funiunfv 7204 difex2 7716 undom 9006 domss2 9077 sucdom2 9144 marypha1lem 9360 kmlem11 10090 hashun2 14324 hashun3 14325 cvgcmpce 15760 dprd2da 19950 dpjcntz 19960 dpjdisj 19961 dpjlsm 19962 dpjidcl 19966 ablfac1eu 19981 dfconn2 23282 2ndcdisj2 23320 fixufil 23785 fin1aufil 23795 xrge0gsumle 24698 unmbl 25414 volsup 25433 mbfss 25523 itg2cnlem2 25639 iblss2 25683 amgm 26877 wilthlem2 26955 ftalem3 26961 rpvmasum2 27399 noetasuplem4 27624 noetainflem4 27628 esumpad 34018 srcmpltd 35043 imadifss 37562 elrfi 42655 oaun2 43343 oaun3 43344 meaunle 46435 dfclnbgr4 47798 clnbupgr 47807 |
| Copyright terms: Public domain | W3C validator |