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

Theorem inundif 3868
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 3650 . . . 4  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
2 eldif 3449 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2orbi12i 521 . . 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 951 . . 3  |-  ( x  e.  A  <->  ( (
x  e.  A  /\  x  e.  B )  \/  ( x  e.  A  /\  -.  x  e.  B
) ) )
53, 4bitr4i 252 . 2  |-  ( ( x  e.  ( A  i^i  B )  \/  x  e.  ( A 
\  B ) )  <-> 
x  e.  A )
65uneqri 3609 1  |-  ( ( A  i^i  B )  u.  ( A  \  B ) )  =  A
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    \/ wo 368    /\ wa 369    = wceq 1370    e. wcel 1758    \ cdif 3436    u. cun 3437    i^i cin 3438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-dif 3442  df-un 3444  df-in 3446
This theorem is referenced by:  resasplit  5692  fresaun  5693  fresaunres2  5694  ixpfi2  7723  hashun3  12268  prmreclem2  14099  mvdco  16073  sylow2a  16242  ablfac1eu  16699  basdif0  18693  neitr  18919  cmpfi  19146  ptbasfi  19289  ptcnplem  19329  fin1aufil  19640  ismbl2  21145  volinun  21163  voliunlem2  21168  mbfeqalem  21256  itg2cnlem2  21376  dvres2lem  21521  imadifxp  26110  ofpreima2  26156  partfun  26164  resf1o  26201  measun  26790  measunl  26795  sibfof  26890  probdif  26967
  Copyright terms: Public domain W3C validator