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

Theorem undif2 4077
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4073). 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 3790 . 2 (𝐴 ∪ (𝐵𝐴)) = ((𝐵𝐴) ∪ 𝐴)
2 undif1 4076 . 2 ((𝐵𝐴) ∪ 𝐴) = (𝐵𝐴)
3 uncom 3790 . 2 (𝐵𝐴) = (𝐴𝐵)
41, 2, 33eqtri 2677 1 (𝐴 ∪ (𝐵𝐴)) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  cdif 3604  cun 3605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949
This theorem is referenced by:  undif  4082  dfif5  4135  funiunfv  6546  difex2  7011  undom  8089  domss2  8160  sucdom2  8197  unfi  8268  marypha1lem  8380  kmlem11  9020  hashun2  13210  hashun3  13211  cvgcmpce  14594  dprd2da  18487  dpjcntz  18497  dpjdisj  18498  dpjlsm  18499  dpjidcl  18503  ablfac1eu  18518  dfconn2  21270  2ndcdisj2  21308  fixufil  21773  fin1aufil  21783  xrge0gsumle  22683  unmbl  23351  volsup  23370  mbfss  23458  itg2cnlem2  23574  iblss2  23617  amgm  24762  wilthlem2  24840  ftalem3  24846  rpvmasum2  25246  esumpad  30245  noetalem3  31990  noetalem4  31991  imadifss  33514  elrfi  37574  meaunle  40999
  Copyright terms: Public domain W3C validator