Theorem undif2 4476

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

Syntax hints:   = wceq 1539   ∖ cdif 3947   ∪ cun 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333

This theorem is referenced by:  undif  4481  dfif5  4541  funiunfv  7269  difex2  7781  undom  9100  undomOLD  9101  sucdom2OLD  9123  domss2  9177  sucdom2  9244  marypha1lem  9474  kmlem11  10202  hashun2  14423  hashun3  14424  cvgcmpce  15855  dprd2da  20063  dpjcntz  20073  dpjdisj  20074  dpjlsm  20075  dpjidcl  20079  ablfac1eu  20094  dfconn2  23428  2ndcdisj2  23466  fixufil  23931  fin1aufil  23941  xrge0gsumle  24856  unmbl  25573  volsup  25592  mbfss  25682  itg2cnlem2  25798  iblss2  25842  amgm  27035  wilthlem2  27113  ftalem3  27119  rpvmasum2  27557  noetasuplem4  27782  noetainflem4  27786  esumpad  34057  srcmpltd  35095  imadifss  37603  elrfi  42710  oaun2  43399  oaun3  43400  meaunle  46484  dfclnbgr4  47816  clnbupgr  47825