Theorem undif2 4431

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

Syntax hints:   = wceq 1542   ∖ cdif 3900   ∪ cun 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288

This theorem is referenced by:  undif  4436  dfif5  4498  funiunfv  7204  difex2  7715  undom  9005  domss2  9076  sucdom2  9139  marypha1lem  9348  kmlem11  10083  hashun2  14318  hashun3  14319  cvgcmpce  15753  dprd2da  19985  dpjcntz  19995  dpjdisj  19996  dpjlsm  19997  dpjidcl  20001  ablfac1eu  20016  dfconn2  23375  2ndcdisj2  23413  fixufil  23878  fin1aufil  23888  xrge0gsumle  24790  unmbl  25506  volsup  25525  mbfss  25615  itg2cnlem2  25731  iblss2  25775  amgm  26969  wilthlem2  27047  ftalem3  27053  rpvmasum2  27491  noetasuplem4  27716  noetainflem4  27720  esumpad  34233  srcmpltd  35256  imadifss  37846  elrfi  43051  oaun2  43738  oaun3  43739  meaunle  46822  dfclnbgr4  48184  clnbupgr  48193