![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inundif | Structured version Visualization version GIF version |
Description: The intersection and class difference of a class with another class unite to give the original class. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
inundif | ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin 3927 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | eldif 3921 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | orbi12i 914 | . . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) |
4 | pm4.42 1053 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) | |
5 | 3, 4 | bitr4i 278 | . 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴) |
6 | 5 | uneqri 4112 | 1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 397 ∨ wo 846 = wceq 1542 ∈ wcel 2107 ∖ cdif 3908 ∪ cun 3909 ∩ cin 3910 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3448 df-dif 3914 df-un 3916 df-in 3918 |
This theorem is referenced by: iunxdif3 5056 partfun 6649 resasplit 6713 fresaun 6714 fresaunres2 6715 ixpfi2 9295 hashun3 14285 prmreclem2 16790 mvdco 19228 sylow2a 19402 ablfac1eu 19853 basdif0 22306 neitr 22534 cmpfi 22762 ptbasfi 22935 ptcnplem 22975 fin1aufil 23286 ismbl2 24894 volinun 24913 voliunlem2 24918 mbfeqalem2 25009 itg2cnlem2 25130 dvres2lem 25277 indifundif 31455 imadifxp 31522 ofpreima2 31585 resf1o 31650 gsummptres 31897 tocyccntz 31996 indsumin 32624 measun 32813 measunl 32818 inelcarsg 32914 carsgclctun 32924 sibfof 32943 probdif 33023 hgt750lemd 33264 mthmpps 34179 clcnvlem 41902 radcnvrat 42601 sumnnodd 43878 ovolsplit 44236 omelesplit 44766 ovnsplit 44896 |
Copyright terms: Public domain | W3C validator |