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

Theorem undif2 3543
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3539). 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 3332 . 2  |-  ( A  u.  ( B  \  A ) )  =  ( ( B  \  A )  u.  A
)
2 undif1 3542 . 2  |-  ( ( B  \  A )  u.  A )  =  ( B  u.  A
)
3 uncom 3332 . 2  |-  ( B  u.  A )  =  ( A  u.  B
)
41, 2, 33eqtri 2320 1  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1632    \ cdif 3162    u. cun 3163
This theorem is referenced by:  undif  3547  dfif5  3590  difex2  4541  funiunfv  5790  undom  6966  domss2  7036  sucdom2  7073  unfi  7140  marypha1lem  7202  kmlem11  7802  hashun2  11381  hashun3  11382  cvgcmpce  12292  dprd2da  15293  dpjcntz  15303  dpjdisj  15304  dpjlsm  15305  dpjidcl  15309  ablfac1eu  15324  dfcon2  17161  2ndcdisj2  17199  fixufil  17633  fin1aufil  17643  xrge0gsumle  18354  unmbl  18911  volsup  18929  mbfss  19017  itg2cnlem2  19133  iblss2  19176  amgm  20301  wilthlem2  20323  ftalem3  20328  rpvmasum2  20677  elrfi  26872
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469
  Copyright terms: Public domain W3C validator