Theorem undif2 4500

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

Syntax hints:   = wceq 1537   ∖ cdif 3973   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353

This theorem is referenced by:  undif  4505  dfif5  4564  funiunfv  7285  difex2  7795  undom  9125  undomOLD  9126  sucdom2OLD  9148  domss2  9202  sucdom2  9269  marypha1lem  9502  kmlem11  10230  hashun2  14432  hashun3  14433  cvgcmpce  15866  dprd2da  20086  dpjcntz  20096  dpjdisj  20097  dpjlsm  20098  dpjidcl  20102  ablfac1eu  20117  dfconn2  23448  2ndcdisj2  23486  fixufil  23951  fin1aufil  23961  xrge0gsumle  24874  unmbl  25591  volsup  25610  mbfss  25700  itg2cnlem2  25817  iblss2  25861  amgm  27052  wilthlem2  27130  ftalem3  27136  rpvmasum2  27574  noetasuplem4  27799  noetainflem4  27803  esumpad  34019  srcmpltd  35056  imadifss  37555  elrfi  42650  oaun2  43343  oaun3  43344  meaunle  46385  dfclnbgr4  47698  clnbupgr  47706