![]() |
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 3978 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | eldif 3972 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | orbi12i 914 | . . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) |
4 | pm4.42 1053 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) | |
5 | 3, 4 | bitr4i 278 | . 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴) |
6 | 5 | uneqri 4165 | 1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 395 ∨ wo 847 = wceq 1536 ∈ wcel 2105 ∖ cdif 3959 ∪ cun 3960 ∩ cin 3961 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 |
This theorem is referenced by: iunxdif3 5099 partfun 6715 resasplit 6778 fresaun 6779 fresaunres2 6780 ixpfi2 9387 hashun3 14419 prmreclem2 16950 mvdco 19477 sylow2a 19651 ablfac1eu 20107 basdif0 22975 neitr 23203 cmpfi 23431 ptbasfi 23604 ptcnplem 23644 fin1aufil 23955 ismbl2 25575 volinun 25594 voliunlem2 25599 mbfeqalem2 25690 itg2cnlem2 25811 dvres2lem 25959 indifundif 32551 imadifxp 32620 ofpreima2 32682 resf1o 32747 gsummptres 33037 tocyccntz 33146 indsumin 34002 measun 34191 measunl 34196 inelcarsg 34292 carsgclctun 34302 sibfof 34321 probdif 34401 hgt750lemd 34641 mthmpps 35566 clcnvlem 43612 radcnvrat 44309 sumnnodd 45585 ovolsplit 45943 omelesplit 46473 ovnsplit 46603 |
Copyright terms: Public domain | W3C validator |