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

Theorem inundif 3745
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 3527 . . . 4  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
2 eldif 3326 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2orbi12i 518 . . 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 944 . . 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 3486 1  |-  ( ( A  i^i  B )  u.  ( A  \  B ) )  =  A
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    \/ wo 368    /\ wa 369    = wceq 1362    e. wcel 1755    \ cdif 3313    u. cun 3314    i^i cin 3315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319  df-un 3321  df-in 3323
This theorem is referenced by:  resasplit  5569  fresaun  5570  fresaunres2  5571  ixpfi2  7597  hashun3  12130  prmreclem2  13960  mvdco  15930  sylow2a  16097  ablfac1eu  16547  basdif0  18399  neitr  18625  cmpfi  18852  ptbasfi  18995  ptcnplem  19035  fin1aufil  19346  ismbl2  20851  volinun  20868  voliunlem2  20873  mbfeqalem  20961  itg2cnlem2  21081  dvres2lem  21226  imadifxp  25762  ofpreima2  25808  partfun  25816  resf1o  25854  measun  26478  measunl  26483  sibfof  26573  probdif  26650
  Copyright terms: Public domain W3C validator