|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > difun2 | Structured version Visualization version GIF version | ||
| Description: Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) | 
| Ref | Expression | 
|---|---|
| difun2 | ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | difundir 4290 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) | |
| 2 | difid 4375 | . . 3 ⊢ (𝐵 ∖ 𝐵) = ∅ | |
| 3 | 2 | uneq2i 4164 | . 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅) | 
| 4 | un0 4393 | . 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵) | |
| 5 | 1, 3, 4 | 3eqtri 2768 | 1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: = wceq 1539 ∖ cdif 3947 ∪ cun 3948 ∅c0 4332 | 
| 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-nul 4333 | 
| This theorem is referenced by: undif5 4484 uneqdifeq 4492 difprsn1 4799 orddif 6479 domunsncan 9113 elfiun 9471 hartogslem1 9583 cantnfp1lem3 9721 dju1dif 10214 infdju1 10231 ssxr 11331 dfn2 12541 incexclem 15873 mreexmrid 17687 lbsextlem4 21164 ufprim 23918 volun 25581 i1f1 25726 itgioo 25852 itgsplitioo 25874 plyeq0lem 26250 jensen 27033 difeq 32538 fzdif2 32793 fzodif2 32794 pmtrcnel2 33111 measun 34213 carsgclctunlem1 34320 carsggect 34321 chtvalz 34645 elmrsubrn 35526 mrsubvrs 35528 pibt2 37419 finixpnum 37613 lindsadd 37621 lindsenlbs 37623 poimirlem2 37630 poimirlem4 37632 poimirlem6 37634 poimirlem7 37635 poimirlem8 37636 poimirlem11 37639 poimirlem12 37640 poimirlem13 37641 poimirlem14 37642 poimirlem16 37644 poimirlem18 37646 poimirlem19 37647 poimirlem21 37649 poimirlem23 37651 poimirlem27 37655 poimirlem30 37658 asindmre 37711 disjresundif 38245 kelac2 43082 pwfi2f1o 43113 iccdifioo 45533 iccdifprioo 45534 hoiprodp1 46608 | 
| Copyright terms: Public domain | W3C validator |