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 4206 | . . 3 ⊢ (𝐵 ∩ 𝐶) = (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) | |
2 | 1 | difeq2i 4059 | . 2 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) |
3 | indi 4213 | . . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) | |
4 | dfin2 4200 | . . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) | |
5 | invdif 4208 | . . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) | |
6 | invdif 4208 | . . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶) | |
7 | 5, 6 | uneq12i 4100 | . . 3 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) |
8 | 3, 4, 7 | 3eqtr3i 2776 | . 2 ⊢ (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) |
9 | 2, 8 | eqtri 2768 | 1 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 Vcvv 3431 ∖ cdif 3889 ∪ cun 3890 ∩ cin 3891 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-ext 2711 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1545 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-rab 3075 df-v 3433 df-dif 3895 df-un 3897 df-in 3899 |
This theorem is referenced by: difdif2 4226 indm 4228 fndifnfp 7045 dprddisj2 19653 fctop 22165 cctop 22167 mretopd 22254 restcld 22334 cfinfil 23055 csdfil 23056 indifundif 30882 difres 30948 unelcarsg 32288 clsk3nimkb 41632 ntrclskb 41661 ntrclsk3 41662 ntrclsk13 41663 salincl 43846 iscnrm3rlem1 46213 |
Copyright terms: Public domain | W3C validator |