Theorem undif2 4443

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

Syntax hints:   = wceq 1540   ∖ cdif 3914   ∪ cun 3915

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300

This theorem is referenced by:  undif  4448  dfif5  4508  funiunfv  7225  difex2  7739  undom  9033  undomOLD  9034  sucdom2OLD  9056  domss2  9106  sucdom2  9173  marypha1lem  9391  kmlem11  10121  hashun2  14355  hashun3  14356  cvgcmpce  15791  dprd2da  19981  dpjcntz  19991  dpjdisj  19992  dpjlsm  19993  dpjidcl  19997  ablfac1eu  20012  dfconn2  23313  2ndcdisj2  23351  fixufil  23816  fin1aufil  23826  xrge0gsumle  24729  unmbl  25445  volsup  25464  mbfss  25554  itg2cnlem2  25670  iblss2  25714  amgm  26908  wilthlem2  26986  ftalem3  26992  rpvmasum2  27430  noetasuplem4  27655  noetainflem4  27659  esumpad  34052  srcmpltd  35077  imadifss  37596  elrfi  42689  oaun2  43377  oaun3  43378  meaunle  46469  dfclnbgr4  47829  clnbupgr  47838