Theorem undif2 4425

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

Syntax hints:   = wceq 1541   ∖ cdif 3897   ∪ cun 3898

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 2112  ax-9 2120  ax-ext 2702

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 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282

This theorem is referenced by:  undif  4430  dfif5  4490  funiunfv  7177  difex2  7688  undom  8973  domss2  9044  sucdom2  9107  marypha1lem  9312  kmlem11  10044  hashun2  14282  hashun3  14283  cvgcmpce  15717  dprd2da  19949  dpjcntz  19959  dpjdisj  19960  dpjlsm  19961  dpjidcl  19965  ablfac1eu  19980  dfconn2  23327  2ndcdisj2  23365  fixufil  23830  fin1aufil  23840  xrge0gsumle  24742  unmbl  25458  volsup  25477  mbfss  25567  itg2cnlem2  25683  iblss2  25727  amgm  26921  wilthlem2  26999  ftalem3  27005  rpvmasum2  27443  noetasuplem4  27668  noetainflem4  27672  esumpad  34058  srcmpltd  35082  imadifss  37614  elrfi  42706  oaun2  43393  oaun3  43394  meaunle  46481  dfclnbgr4  47834  clnbupgr  47843