Theorem undif2 4436

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4431). 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 4117	. 2 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∪ 𝐴)
2		undif1 4435	. 2 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴)
3		uncom 4117	. 2 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵)
4	1, 2, 3	3eqtri 2756	1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1540   ∖ cdif 3908   ∪ cun 3909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293

This theorem is referenced by:  undif  4441  dfif5  4501  funiunfv  7204  difex2  7716  undom  9006  domss2  9077  sucdom2  9144  marypha1lem  9360  kmlem11  10090  hashun2  14324  hashun3  14325  cvgcmpce  15760  dprd2da  19950  dpjcntz  19960  dpjdisj  19961  dpjlsm  19962  dpjidcl  19966  ablfac1eu  19981  dfconn2  23282  2ndcdisj2  23320  fixufil  23785  fin1aufil  23795  xrge0gsumle  24698  unmbl  25414  volsup  25433  mbfss  25523  itg2cnlem2  25639  iblss2  25683  amgm  26877  wilthlem2  26955  ftalem3  26961  rpvmasum2  27399  noetasuplem4  27624  noetainflem4  27628  esumpad  34018  srcmpltd  35043  imadifss  37562  elrfi  42655  oaun2  43343  oaun3  43344  meaunle  46435  dfclnbgr4  47798  clnbupgr  47807