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

Theorem inundif 3650
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 3474 . . . 4  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
2 eldif 3274 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2orbi12i 508 . . 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 927 . . 3  |-  ( x  e.  A  <->  ( (
x  e.  A  /\  x  e.  B )  \/  ( x  e.  A  /\  -.  x  e.  B
) ) )
53, 4bitr4i 244 . 2  |-  ( ( x  e.  ( A  i^i  B )  \/  x  e.  ( A 
\  B ) )  <-> 
x  e.  A )
65uneqri 3433 1  |-  ( ( A  i^i  B )  u.  ( A  \  B ) )  =  A
Colors of variables: wff set class
Syntax hints:   -. wn 3    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1717    \ cdif 3261    u. cun 3262    i^i cin 3263
This theorem is referenced by:  resasplit  5554  fresaun  5555  fresaunres2  5556  ixpfi2  7341  hashun3  11586  prmreclem2  13213  sylow2a  15181  ablfac1eu  15559  basdif0  16942  neitr  17167  cmpfi  17394  ptbasfi  17535  ptcnplem  17575  fin1aufil  17886  ismbl2  19291  volinun  19308  voliunlem2  19313  mbfeqalem  19402  itg2cnlem2  19522  dvres2lem  19665  imadifxp  23882  partfun  23929  measun  24360  measunl  24365  probdif  24458  mvdco  27058
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-dif 3267  df-un 3269  df-in 3271
  Copyright terms: Public domain W3C validator