![]() |
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 3947 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | eldif 3733 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | orbi12i 900 | . . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) |
4 | pm4.42 1040 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) | |
5 | 3, 4 | bitr4i 267 | . 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴) |
6 | 5 | uneqri 3906 | 1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 382 ∨ wo 836 = wceq 1631 ∈ wcel 2145 ∖ cdif 3720 ∪ cun 3721 ∩ cin 3722 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 |
This theorem is referenced by: iunxdif3 4740 resasplit 6212 fresaun 6213 fresaunres2 6214 ixpfi2 8418 hashun3 13368 prmreclem2 15821 mvdco 18065 sylow2a 18234 ablfac1eu 18673 basdif0 20971 neitr 21198 cmpfi 21425 ptbasfi 21598 ptcnplem 21638 fin1aufil 21949 ismbl2 23508 volinun 23527 voliunlem2 23532 mbfeqalem 23622 itg2cnlem2 23742 dvres2lem 23887 indifundif 29687 imadifxp 29745 ofpreima2 29799 partfun 29808 resf1o 29838 gsummptres 30117 indsumin 30417 measun 30607 measunl 30612 inelcarsg 30706 carsgclctun 30716 sibfof 30735 probdif 30815 hgt750lemd 31059 mthmpps 31810 clcnvlem 38449 radcnvrat 39032 sumnnodd 40373 ovolsplit 40715 omelesplit 41245 ovnsplit 41375 |
Copyright terms: Public domain | W3C validator |