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

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

Proof of Theorem undif2
StepHypRef Expression
1 uncom 3319 . 2
2 undif1 3529 . 2
3 uncom 3319 . 2
41, 2, 33eqtri 2307 1
 Colors of variables: wff set class Syntax hints:   wceq 1623   cdif 3149   cun 3150 This theorem is referenced by:  undif  3534  dfif5  3577  difex2  4525  funiunfv  5774  undom  6950  domss2  7020  sucdom2  7057  unfi  7124  marypha1lem  7186  kmlem11  7786  hashun2  11365  hashun3  11366  cvgcmpce  12276  dprd2da  15277  dpjcntz  15287  dpjdisj  15288  dpjlsm  15289  dpjidcl  15293  ablfac1eu  15308  dfcon2  17145  2ndcdisj2  17183  fixufil  17617  fin1aufil  17627  xrge0gsumle  18338  unmbl  18895  volsup  18913  mbfss  19001  itg2cnlem2  19117  iblss2  19160  amgm  20285  wilthlem2  20307  ftalem3  20312  rpvmasum2  20661  elrfi  26769 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456
 Copyright terms: Public domain W3C validator