|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > difundir | Structured version Visualization version GIF version | ||
| Description: Distributive law for class difference. (Contributed by NM, 17-Aug-2004.) | 
| Ref | Expression | 
|---|---|
| difundir | ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | indir 4285 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) | |
| 2 | invdif 4278 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶) | |
| 3 | invdif 4278 | . . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶) | |
| 4 | invdif 4278 | . . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶) | |
| 5 | 3, 4 | uneq12i 4165 | . 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) | 
| 6 | 1, 2, 5 | 3eqtr3i 2772 | 1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: = wceq 1539 Vcvv 3479 ∖ cdif 3947 ∪ cun 3948 ∩ cin 3949 | 
| 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-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 | 
| This theorem is referenced by: dfsymdif3 4305 difun2 4480 diftpsn3 4801 strleun 17195 setsfun0 17210 mreexmrid 17687 mreexexlem2d 17689 mvdco 19464 dprd2da 20063 dmdprdsplit2lem 20066 ablfac1eulem 20093 lbsextlem4 21164 opsrtoslem2 22081 nulmbl2 25572 uniioombllem3 25621 sltlpss 27946 slelss 27947 ex-dif 30443 indifundif 32544 imadifxp 32615 fzodif1 32795 chnccats1 33006 cycpmrn 33164 ballotlemfp1 34495 ballotlemgun 34528 onint1 36451 lindsadd 37621 lindsenlbs 37623 poimirlem2 37630 poimirlem6 37634 poimirlem7 37635 poimirlem8 37636 poimirlem22 37650 dvmptfprodlem 45964 fourierdlem102 46228 fourierdlem114 46240 caragenuncllem 46532 carageniuncllem1 46541 | 
| Copyright terms: Public domain | W3C validator |