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 4169 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | eldif 3946 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | orbi12i 911 | . . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) |
4 | pm4.42 1048 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) | |
5 | 3, 4 | bitr4i 280 | . 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴) |
6 | 5 | uneqri 4127 | 1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 398 ∨ wo 843 = wceq 1533 ∈ wcel 2110 ∖ cdif 3933 ∪ cun 3934 ∩ cin 3935 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-dif 3939 df-un 3941 df-in 3943 |
This theorem is referenced by: iunxdif3 5010 resasplit 6543 fresaun 6544 fresaunres2 6545 ixpfi2 8816 hashun3 13739 prmreclem2 16247 mvdco 18567 sylow2a 18738 ablfac1eu 19189 basdif0 21555 neitr 21782 cmpfi 22010 ptbasfi 22183 ptcnplem 22223 fin1aufil 22534 ismbl2 24122 volinun 24141 voliunlem2 24146 mbfeqalem2 24237 itg2cnlem2 24357 dvres2lem 24502 indifundif 30279 imadifxp 30345 ofpreima2 30405 partfun 30415 resf1o 30460 gsummptres 30685 tocyccntz 30781 indsumin 31276 measun 31465 measunl 31470 inelcarsg 31564 carsgclctun 31574 sibfof 31593 probdif 31673 hgt750lemd 31914 mthmpps 32824 clcnvlem 39976 radcnvrat 40639 sumnnodd 41903 ovolsplit 42266 omelesplit 42793 ovnsplit 42923 |
Copyright terms: Public domain | W3C validator |