Theorem undif2 4483

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

Assertion

Ref	Expression
undif2	⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)

Proof of Theorem undif2

Step	Hyp	Ref	Expression
1		uncom 4168	. 2 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∪ 𝐴)
2		undif1 4482	. 2 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴)
3		uncom 4168	. 2 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵)
4	1, 2, 3	3eqtri 2767	1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1537   ∖ cdif 3960   ∪ cun 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340

This theorem is referenced by:  undif  4488  dfif5  4547  funiunfv  7268  difex2  7779  undom  9098  undomOLD  9099  sucdom2OLD  9121  domss2  9175  sucdom2  9241  marypha1lem  9471  kmlem11  10199  hashun2  14419  hashun3  14420  cvgcmpce  15851  dprd2da  20077  dpjcntz  20087  dpjdisj  20088  dpjlsm  20089  dpjidcl  20093  ablfac1eu  20108  dfconn2  23443  2ndcdisj2  23481  fixufil  23946  fin1aufil  23956  xrge0gsumle  24869  unmbl  25586  volsup  25605  mbfss  25695  itg2cnlem2  25812  iblss2  25856  amgm  27049  wilthlem2  27127  ftalem3  27133  rpvmasum2  27571  noetasuplem4  27796  noetainflem4  27800  esumpad  34036  srcmpltd  35073  imadifss  37582  elrfi  42682  oaun2  43371  oaun3  43372  meaunle  46420  dfclnbgr4  47749  clnbupgr  47758