Theorem undif2 4410

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

Syntax hints:   = wceq 1539   ∖ cdif 3884   ∪ cun 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257

This theorem is referenced by:  undif  4415  dfif5  4475  funiunfv  7121  difex2  7610  undom  8846  undomOLD  8847  sucdom2OLD  8869  domss2  8923  sucdom2  8989  unfiOLD  9081  marypha1lem  9192  kmlem11  9916  hashun2  14098  hashun3  14099  cvgcmpce  15530  dprd2da  19645  dpjcntz  19655  dpjdisj  19656  dpjlsm  19657  dpjidcl  19661  ablfac1eu  19676  dfconn2  22570  2ndcdisj2  22608  fixufil  23073  fin1aufil  23083  xrge0gsumle  23996  unmbl  24701  volsup  24720  mbfss  24810  itg2cnlem2  24927  iblss2  24970  amgm  26140  wilthlem2  26218  ftalem3  26224  rpvmasum2  26660  esumpad  32023  srcmpltd  33054  noetasuplem4  33939  noetainflem4  33943  imadifss  35752  elrfi  40516  meaunle  44002