Theorem undif2 4441

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

Syntax hints:   = wceq 1541   ∖ cdif 3910   ∪ cun 3911

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288

This theorem is referenced by:  undif  4446  dfif5  4507  funiunfv  7200  difex2  7699  undom  9010  undomOLD  9011  sucdom2OLD  9033  domss2  9087  sucdom2  9157  unfiOLD  9264  marypha1lem  9378  kmlem11  10105  hashun2  14293  hashun3  14294  cvgcmpce  15714  dprd2da  19835  dpjcntz  19845  dpjdisj  19846  dpjlsm  19847  dpjidcl  19851  ablfac1eu  19866  dfconn2  22807  2ndcdisj2  22845  fixufil  23310  fin1aufil  23320  xrge0gsumle  24233  unmbl  24938  volsup  24957  mbfss  25047  itg2cnlem2  25164  iblss2  25207  amgm  26377  wilthlem2  26455  ftalem3  26461  rpvmasum2  26897  noetasuplem4  27121  noetainflem4  27125  esumpad  32743  srcmpltd  33775  imadifss  36126  elrfi  41075  oaun2  41774  oaun3  41775  meaunle  44825