![]() |
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 4240 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) | |
2 | invdif 4233 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶) | |
3 | invdif 4233 | . . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶) | |
4 | invdif 4233 | . . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶) | |
5 | 3, 4 | uneq12i 4126 | . 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) |
6 | 1, 2, 5 | 3eqtr3i 2767 | 1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 Vcvv 3446 ∖ cdif 3910 ∪ cun 3911 ∩ cin 3912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3406 df-v 3448 df-dif 3916 df-un 3918 df-in 3920 |
This theorem is referenced by: dfsymdif3 4261 difun2 4445 diftpsn3 4767 strleun 17040 setsfun0 17055 mreexmrid 17537 mreexexlem2d 17539 mvdco 19241 dprd2da 19835 dmdprdsplit2lem 19838 ablfac1eulem 19865 lbsextlem4 20681 opsrtoslem2 21500 nulmbl2 24937 uniioombllem3 24986 sltlpss 27279 ex-dif 29430 indifundif 31516 imadifxp 31586 fzodif1 31764 cycpmrn 32062 ballotlemfp1 33180 ballotlemgun 33213 onint1 34997 lindsadd 36144 lindsenlbs 36146 poimirlem2 36153 poimirlem6 36157 poimirlem7 36158 poimirlem8 36159 poimirlem22 36173 dvmptfprodlem 44305 fourierdlem102 44569 fourierdlem114 44581 caragenuncllem 44873 carageniuncllem1 44882 |
Copyright terms: Public domain | W3C validator |