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

Theorem inundif 3818
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  |-  ( ( A  i^i  B )  u.  ( A  \  B ) )  =  A

Proof of Theorem inundif
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elin 3592 . . . 4  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
2 eldif 3389 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2orbi12i 523 . . 3  |-  ( ( x  e.  ( A  i^i  B )  \/  x  e.  ( A 
\  B ) )  <-> 
( ( x  e.  A  /\  x  e.  B )  \/  (
x  e.  A  /\  -.  x  e.  B
) ) )
4 pm4.42 968 . . 3  |-  ( x  e.  A  <->  ( (
x  e.  A  /\  x  e.  B )  \/  ( x  e.  A  /\  -.  x  e.  B
) ) )
53, 4bitr4i 255 . 2  |-  ( ( x  e.  ( A  i^i  B )  \/  x  e.  ( A 
\  B ) )  <-> 
x  e.  A )
65uneqri 3551 1  |-  ( ( A  i^i  B )  u.  ( A  \  B ) )  =  A
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1872    \ cdif 3376    u. cun 3377    i^i cin 3378
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-dif 3382  df-un 3384  df-in 3386
This theorem is referenced by:  resasplit  5713  fresaun  5714  fresaunres2  5715  ixpfi2  7825  hashun3  12513  prmreclem2  14804  mvdco  17029  sylow2a  17214  ablfac1eu  17649  basdif0  19910  neitr  20138  cmpfi  20365  ptbasfi  20538  ptcnplem  20578  fin1aufil  20889  ismbl2  22423  volinun  22441  voliunlem2  22446  mbfeqalem  22540  itg2cnlem2  22662  dvres2lem  22807  indifundif  28095  iunxdif3  28121  imadifxp  28158  ofpreima2  28215  partfun  28224  resf1o  28265  gsummptres  28499  measun  28985  measunl  28990  inelcarsg  29095  carsgclctun  29105  sibfof  29125  probdif  29205  mthmpps  30172  clcnvlem  36143  radcnvrat  36576  sumnnodd  37593  omelesplit  38190
  Copyright terms: Public domain W3C validator