| 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 3967 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
| 2 | eldif 3961 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
| 3 | 1, 2 | orbi12i 915 | . . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) |
| 4 | pm4.42 1054 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) | |
| 5 | 3, 4 | bitr4i 278 | . 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴) |
| 6 | 5 | uneqri 4156 | 1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ∧ wa 395 ∨ wo 848 = wceq 1540 ∈ wcel 2108 ∖ 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-v 3482 df-dif 3954 df-un 3956 df-in 3958 |
| This theorem is referenced by: iunxdif3 5095 partfun 6715 resasplit 6778 fresaun 6779 fresaunres2 6780 ixpfi2 9390 hashun3 14423 prmreclem2 16955 mvdco 19463 sylow2a 19637 ablfac1eu 20093 basdif0 22960 neitr 23188 cmpfi 23416 ptbasfi 23589 ptcnplem 23629 fin1aufil 23940 ismbl2 25562 volinun 25581 voliunlem2 25586 mbfeqalem2 25677 itg2cnlem2 25797 dvres2lem 25945 indifundif 32543 imadifxp 32614 ofpreima2 32676 resf1o 32741 indsumin 32847 gsummptres 33055 tocyccntz 33164 measun 34212 measunl 34217 inelcarsg 34313 carsgclctun 34323 sibfof 34342 probdif 34422 hgt750lemd 34663 mthmpps 35587 clcnvlem 43636 radcnvrat 44333 sumnnodd 45645 ovolsplit 46003 omelesplit 46533 ovnsplit 46663 |
| Copyright terms: Public domain | W3C validator |