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

Theorem undif2 3696
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3692). 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 3483 . 2  |-  ( A  u.  ( B  \  A ) )  =  ( ( B  \  A )  u.  A
)
2 undif1 3695 . 2  |-  ( ( B  \  A )  u.  A )  =  ( B  u.  A
)
3 uncom 3483 . 2  |-  ( B  u.  A )  =  ( A  u.  B
)
41, 2, 33eqtri 2459 1  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1652    \ cdif 3309    u. cun 3310
This theorem is referenced by:  undif  3700  dfif5  3743  difex2  4705  funiunfv  5986  undom  7187  domss2  7257  sucdom2  7294  unfi  7365  marypha1lem  7429  kmlem11  8029  hashun2  11645  hashun3  11646  cvgcmpce  12585  dprd2da  15588  dpjcntz  15598  dpjdisj  15599  dpjlsm  15600  dpjidcl  15604  ablfac1eu  15619  dfcon2  17470  2ndcdisj2  17508  fixufil  17942  fin1aufil  17952  xrge0gsumle  18852  unmbl  19420  volsup  19438  mbfss  19526  itg2cnlem2  19642  iblss2  19685  amgm  20817  wilthlem2  20840  ftalem3  20845  rpvmasum2  21194  elrfi  26685
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621
  Copyright terms: Public domain W3C validator