Theorem undif2 4436

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

Syntax hints:   = wceq 1540   ∖ cdif 3908   ∪ cun 3909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293

This theorem is referenced by:  undif  4441  dfif5  4501  funiunfv  7204  difex2  7716  undom  9006  domss2  9077  sucdom2  9144  marypha1lem  9360  kmlem11  10090  hashun2  14324  hashun3  14325  cvgcmpce  15760  dprd2da  19958  dpjcntz  19968  dpjdisj  19969  dpjlsm  19970  dpjidcl  19974  ablfac1eu  19989  dfconn2  23339  2ndcdisj2  23377  fixufil  23842  fin1aufil  23852  xrge0gsumle  24755  unmbl  25471  volsup  25490  mbfss  25580  itg2cnlem2  25696  iblss2  25740  amgm  26934  wilthlem2  27012  ftalem3  27018  rpvmasum2  27456  noetasuplem4  27681  noetainflem4  27685  esumpad  34038  srcmpltd  35063  imadifss  37582  elrfi  42675  oaun2  43363  oaun3  43364  meaunle  46455  dfclnbgr4  47818  clnbupgr  47827