Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  inundif Structured version   Visualization version   GIF version

Theorem inundif 4023
 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.)
Assertion
Ref Expression
inundif ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴

Proof of Theorem inundif
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elin 3779 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3569 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 543 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1003 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 267 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 3738 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∨ wo 383   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ∖ cdif 3556   ∪ cun 3557   ∩ cin 3558 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3191  df-dif 3562  df-un 3564  df-in 3566 This theorem is referenced by:  iunxdif3  4577  resasplit  6036  fresaun  6037  fresaunres2  6038  ixpfi2  8215  hashun3  13120  prmreclem2  15552  mvdco  17793  sylow2a  17962  ablfac1eu  18400  basdif0  20677  neitr  20903  cmpfi  21130  ptbasfi  21303  ptcnplem  21343  fin1aufil  21655  ismbl2  23214  volinun  23233  voliunlem2  23238  mbfeqalem  23328  itg2cnlem2  23448  dvres2lem  23593  indifundif  29221  imadifxp  29277  ofpreima2  29327  partfun  29336  resf1o  29366  gsummptres  29587  measun  30073  measunl  30078  inelcarsg  30172  carsgclctun  30182  sibfof  30201  probdif  30281  mthmpps  31214  clcnvlem  37438  radcnvrat  38022  sumnnodd  39289  ovolsplit  39533  omelesplit  40060  ovnsplit  40190
 Copyright terms: Public domain W3C validator