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

Theorem undif2 3532
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3528). 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 3321 . 2  |-  ( A  u.  ( B  \  A ) )  =  ( ( B  \  A )  u.  A
)
2 undif1 3531 . 2  |-  ( ( B  \  A )  u.  A )  =  ( B  u.  A
)
3 uncom 3321 . 2  |-  ( B  u.  A )  =  ( A  u.  B
)
41, 2, 33eqtri 2309 1  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1624    \ cdif 3151    u. cun 3152
This theorem is referenced by:  undif  3536  dfif5  3579  difex2  4525  funiunfv  5736  undom  6946  domss2  7016  sucdom2  7053  unfi  7120  marypha1lem  7182  kmlem11  7782  hashun2  11360  hashun3  11361  cvgcmpce  12271  dprd2da  15272  dpjcntz  15282  dpjdisj  15283  dpjlsm  15284  dpjidcl  15288  ablfac1eu  15303  dfcon2  17140  2ndcdisj2  17178  fixufil  17612  fin1aufil  17622  xrge0gsumle  18333  unmbl  18890  volsup  18908  mbfss  18996  itg2cnlem2  19112  iblss2  19155  amgm  20280  wilthlem2  20302  ftalem3  20307  rpvmasum2  20656  elrfi  26169
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458
  Copyright terms: Public domain W3C validator