Theorem undif2 4424

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

Syntax hints:   = wceq 1541   ∖ cdif 3894   ∪ cun 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281

This theorem is referenced by:  undif  4429  dfif5  4489  funiunfv  7182  difex2  7693  undom  8978  domss2  9049  sucdom2  9112  marypha1lem  9317  kmlem11  10052  hashun2  14290  hashun3  14291  cvgcmpce  15725  dprd2da  19956  dpjcntz  19966  dpjdisj  19967  dpjlsm  19968  dpjidcl  19972  ablfac1eu  19987  dfconn2  23334  2ndcdisj2  23372  fixufil  23837  fin1aufil  23847  xrge0gsumle  24749  unmbl  25465  volsup  25484  mbfss  25574  itg2cnlem2  25690  iblss2  25734  amgm  26928  wilthlem2  27006  ftalem3  27012  rpvmasum2  27450  noetasuplem4  27675  noetainflem4  27679  esumpad  34068  srcmpltd  35092  imadifss  37645  elrfi  42797  oaun2  43484  oaun3  43485  meaunle  46572  dfclnbgr4  47934  clnbupgr  47943