|   | 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 4471). 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 4157 | . 2 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∪ 𝐴) | |
| 2 | undif1 4475 | . 2 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴) | |
| 3 | uncom 4157 | . 2 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) | |
| 4 | 1, 2, 3 | 3eqtri 2768 | 1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: = wceq 1539 ∖ cdif 3947 ∪ cun 3948 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 | 
| This theorem is referenced by: undif 4481 dfif5 4541 funiunfv 7269 difex2 7781 undom 9100 undomOLD 9101 sucdom2OLD 9123 domss2 9177 sucdom2 9244 marypha1lem 9474 kmlem11 10202 hashun2 14423 hashun3 14424 cvgcmpce 15855 dprd2da 20063 dpjcntz 20073 dpjdisj 20074 dpjlsm 20075 dpjidcl 20079 ablfac1eu 20094 dfconn2 23428 2ndcdisj2 23466 fixufil 23931 fin1aufil 23941 xrge0gsumle 24856 unmbl 25573 volsup 25592 mbfss 25682 itg2cnlem2 25798 iblss2 25842 amgm 27035 wilthlem2 27113 ftalem3 27119 rpvmasum2 27557 noetasuplem4 27782 noetainflem4 27786 esumpad 34057 srcmpltd 35095 imadifss 37603 elrfi 42710 oaun2 43399 oaun3 43400 meaunle 46484 dfclnbgr4 47816 clnbupgr 47825 | 
| Copyright terms: Public domain | W3C validator |