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

Theorem undif2 3436
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3432). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.)
Assertion
Ref Expression
undif2  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)

Proof of Theorem undif2
StepHypRef Expression
1 uncom 3229 . 2  |-  ( A  u.  ( B  \  A ) )  =  ( ( B  \  A )  u.  A
)
2 undif1 3435 . 2  |-  ( ( B  \  A )  u.  A )  =  ( B  u.  A
)
3 uncom 3229 . 2  |-  ( B  u.  A )  =  ( A  u.  B
)
41, 2, 33eqtri 2277 1  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1619    \ cdif 3075    u. cun 3076
This theorem is referenced by:  undif  3440  dfif5  3482  difex2  4416  funiunfv  5626  undom  6835  domss2  6905  sucdom2  6942  unfi  7009  marypha1lem  7070  kmlem11  7670  hashun2  11243  cvgcmpce  12153  dprd2da  15112  dpjcntz  15122  dpjdisj  15123  dpjlsm  15124  dpjidcl  15128  ablfac1eu  15143  dfcon2  16977  2ndcdisj2  17015  fixufil  17449  fin1aufil  17459  xrge0gsumle  18170  unmbl  18727  volsup  18745  mbfss  18833  itg2cnlem2  18949  iblss2  18992  amgm  20117  wilthlem2  20139  ftalem3  20144  rpvmasum2  20493  elrfi  25935
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363
  Copyright terms: Public domain W3C validator