Theorem undif2 4418

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

Syntax hints:   = wceq 1542   ∖ cdif 3887   ∪ cun 3888

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275

This theorem is referenced by:  undif  4423  dfif5  4484  funiunfv  7197  difex2  7708  undom  8997  domss2  9068  sucdom2  9131  marypha1lem  9340  kmlem11  10077  hashun2  14339  hashun3  14340  cvgcmpce  15775  dprd2da  20013  dpjcntz  20023  dpjdisj  20024  dpjlsm  20025  dpjidcl  20029  ablfac1eu  20044  dfconn2  23397  2ndcdisj2  23435  fixufil  23900  fin1aufil  23910  xrge0gsumle  24812  unmbl  25517  volsup  25536  mbfss  25626  itg2cnlem2  25742  iblss2  25786  amgm  26971  wilthlem2  27049  ftalem3  27055  rpvmasum2  27492  noetasuplem4  27717  noetainflem4  27721  esumpad  34218  srcmpltd  35241  imadifss  37933  elrfi  43143  oaun2  43830  oaun3  43831  meaunle  46913  dfclnbgr4  48315  clnbupgr  48324