![]() |
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 3960 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | eldif 3954 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | orbi12i 912 | . . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) |
4 | pm4.42 1051 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) | |
5 | 3, 4 | bitr4i 277 | . 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴) |
6 | 5 | uneqri 4148 | 1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 394 ∨ wo 845 = wceq 1533 ∈ wcel 2098 ∖ cdif 3941 ∪ cun 3942 ∩ cin 3943 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 |
This theorem is referenced by: iunxdif3 5099 partfun 6703 resasplit 6767 fresaun 6768 fresaunres2 6769 ixpfi2 9376 hashun3 14379 prmreclem2 16889 mvdco 19412 sylow2a 19586 ablfac1eu 20042 basdif0 22900 neitr 23128 cmpfi 23356 ptbasfi 23529 ptcnplem 23569 fin1aufil 23880 ismbl2 25500 volinun 25519 voliunlem2 25524 mbfeqalem2 25615 itg2cnlem2 25736 dvres2lem 25883 indifundif 32400 imadifxp 32470 ofpreima2 32533 resf1o 32594 gsummptres 32856 tocyccntz 32957 indsumin 33772 measun 33961 measunl 33966 inelcarsg 34062 carsgclctun 34072 sibfof 34091 probdif 34171 hgt750lemd 34411 mthmpps 35323 clcnvlem 43195 radcnvrat 43893 sumnnodd 45156 ovolsplit 45514 omelesplit 46044 ovnsplit 46174 |
Copyright terms: Public domain | W3C validator |