|   | 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 4277 | . . 3 ⊢ (𝐵 ∩ 𝐶) = (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) | |
| 2 | 1 | difeq2i 4123 | . 2 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) | 
| 3 | indi 4284 | . . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) | |
| 4 | dfin2 4271 | . . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) | |
| 5 | invdif 4279 | . . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) | |
| 6 | invdif 4279 | . . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶) | |
| 7 | 5, 6 | uneq12i 4166 | . . 3 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) | 
| 8 | 3, 4, 7 | 3eqtr3i 2773 | . 2 ⊢ (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) | 
| 9 | 2, 8 | eqtri 2765 | 1 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: = wceq 1540 Vcvv 3480 ∖ cdif 3948 ∪ cun 3949 ∩ cin 3950 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 | 
| This theorem is referenced by: difdif2 4296 indm 4298 fndifnfp 7196 dprddisj2 20059 fctop 23011 cctop 23013 mretopd 23100 restcld 23180 cfinfil 23901 csdfil 23902 indifundif 32543 difres 32613 unelcarsg 34314 clsk3nimkb 44053 ntrclskb 44082 ntrclsk3 44083 ntrclsk13 44084 salincl 46339 iscnrm3rlem1 48837 | 
| Copyright terms: Public domain | W3C validator |