![]() |
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 3963 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | eldif 3957 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | orbi12i 911 | . . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) |
4 | pm4.42 1050 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) | |
5 | 3, 4 | bitr4i 277 | . 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴) |
6 | 5 | uneqri 4150 | 1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 394 ∨ wo 843 = wceq 1539 ∈ wcel 2104 ∖ cdif 3944 ∪ cun 3945 ∩ cin 3946 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-v 3474 df-dif 3950 df-un 3952 df-in 3954 |
This theorem is referenced by: iunxdif3 5097 partfun 6696 resasplit 6760 fresaun 6761 fresaunres2 6762 ixpfi2 9352 hashun3 14348 prmreclem2 16854 mvdco 19354 sylow2a 19528 ablfac1eu 19984 basdif0 22676 neitr 22904 cmpfi 23132 ptbasfi 23305 ptcnplem 23345 fin1aufil 23656 ismbl2 25276 volinun 25295 voliunlem2 25300 mbfeqalem2 25391 itg2cnlem2 25512 dvres2lem 25659 indifundif 32029 imadifxp 32099 ofpreima2 32158 resf1o 32222 gsummptres 32474 tocyccntz 32573 indsumin 33318 measun 33507 measunl 33512 inelcarsg 33608 carsgclctun 33618 sibfof 33637 probdif 33717 hgt750lemd 33958 mthmpps 34871 clcnvlem 42676 radcnvrat 43375 sumnnodd 44644 ovolsplit 45002 omelesplit 45532 ovnsplit 45662 |
Copyright terms: Public domain | W3C validator |