| 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 19958 dpjcntz 19968 dpjdisj 19969 dpjlsm 19970 dpjidcl 19974 ablfac1eu 19989 dfconn2 23339 2ndcdisj2 23377 fixufil 23842 fin1aufil 23852 xrge0gsumle 24755 unmbl 25471 volsup 25490 mbfss 25580 itg2cnlem2 25696 iblss2 25740 amgm 26934 wilthlem2 27012 ftalem3 27018 rpvmasum2 27456 noetasuplem4 27681 noetainflem4 27685 esumpad 34038 srcmpltd 35063 imadifss 37582 elrfi 42675 oaun2 43363 oaun3 43364 meaunle 46455 dfclnbgr4 47818 clnbupgr 47827 |
| Copyright terms: Public domain | W3C validator |