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

Theorem inundif 3532
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 3358 . . . 4  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
2 eldif 3162 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2orbi12i 507 . . 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 926 . . 3  |-  ( x  e.  A  <->  ( (
x  e.  A  /\  x  e.  B )  \/  ( x  e.  A  /\  -.  x  e.  B
) ) )
53, 4bitr4i 243 . 2  |-  ( ( x  e.  ( A  i^i  B )  \/  x  e.  ( A 
\  B ) )  <-> 
x  e.  A )
65uneqri 3317 1  |-  ( ( A  i^i  B )  u.  ( A  \  B ) )  =  A
Colors of variables: wff set class
Syntax hints:   -. wn 3    \/ wo 357    /\ wa 358    = wceq 1623    e. wcel 1684    \ cdif 3149    u. cun 3150    i^i cin 3151
This theorem is referenced by:  resasplit  5411  fresaun  5412  fresaunres2  5413  ixpfi2  7154  hashun3  11366  prmreclem2  12964  sylow2a  14930  ablfac1eu  15308  basdif0  16691  cmpfi  17135  ptbasfi  17276  ptcnplem  17315  fin1aufil  17627  ismbl2  18886  volinun  18903  voliunlem2  18908  mbfeqalem  18997  itg2cnlem2  19117  dvres2lem  19260  partfun  23240  measxun  23539  probdif  23623  islimrs4  25582  mvdco  27388
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-un 3157  df-in 3159
  Copyright terms: Public domain W3C validator