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

Theorem undif2 4397
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4393). 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 4104 . 2 (𝐴 ∪ (𝐵𝐴)) = ((𝐵𝐴) ∪ 𝐴)
2 undif1 4396 . 2 ((𝐵𝐴) ∪ 𝐴) = (𝐵𝐴)
3 uncom 4104 . 2 (𝐵𝐴) = (𝐴𝐵)
41, 2, 33eqtri 2849 1 (𝐴 ∪ (𝐵𝐴)) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  cdif 3905  cun 3906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-11 2161  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-rab 3139  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266
This theorem is referenced by:  undif  4402  dfif5  4455  funiunfv  6990  difex2  7467  undom  8592  sucdom2  8614  domss2  8664  unfi  8773  marypha1lem  8885  kmlem11  9575  hashun2  13740  hashun3  13741  cvgcmpce  15164  dprd2da  19155  dpjcntz  19165  dpjdisj  19166  dpjlsm  19167  dpjidcl  19171  ablfac1eu  19186  dfconn2  22022  2ndcdisj2  22060  fixufil  22525  fin1aufil  22535  xrge0gsumle  23436  unmbl  24139  volsup  24158  mbfss  24248  itg2cnlem2  24364  iblss2  24407  amgm  25574  wilthlem2  25652  ftalem3  25658  rpvmasum2  26094  esumpad  31388  srcmpltd  32420  noetalem3  33293  noetalem4  33294  imadifss  34990  elrfi  39565  meaunle  43042
  Copyright terms: Public domain W3C validator