![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > difindi | Structured version Visualization version GIF version |
Description: Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
Ref | Expression |
---|---|
difindi | ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfin3 3899 | . . 3 ⊢ (𝐵 ∩ 𝐶) = (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) | |
2 | 1 | difeq2i 3758 | . 2 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) |
3 | indi 3906 | . . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) | |
4 | dfin2 3893 | . . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) | |
5 | invdif 3901 | . . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) | |
6 | invdif 3901 | . . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶) | |
7 | 5, 6 | uneq12i 3798 | . . 3 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) |
8 | 3, 4, 7 | 3eqtr3i 2681 | . 2 ⊢ (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) |
9 | 2, 8 | eqtri 2673 | 1 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 Vcvv 3231 ∖ cdif 3604 ∪ cun 3605 ∩ cin 3606 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 |
This theorem is referenced by: difdif2 3917 indm 3919 fndifnfp 6483 dprddisj2 18484 fctop 20856 cctop 20858 mretopd 20944 restcld 21024 cfinfil 21744 csdfil 21745 indifundif 29482 difres 29539 unelcarsg 30502 clsk3nimkb 38655 ntrclskb 38684 ntrclsk3 38685 ntrclsk13 38686 salincl 40861 |
Copyright terms: Public domain | W3C validator |