Theorem undif2 4429

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

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286

This theorem is referenced by:  undif  4434  dfif5  4496  funiunfv  7194  difex2  7705  undom  8993  domss2  9064  sucdom2  9127  marypha1lem  9336  kmlem11  10071  hashun2  14306  hashun3  14307  cvgcmpce  15741  dprd2da  19973  dpjcntz  19983  dpjdisj  19984  dpjlsm  19985  dpjidcl  19989  ablfac1eu  20004  dfconn2  23363  2ndcdisj2  23401  fixufil  23866  fin1aufil  23876  xrge0gsumle  24778  unmbl  25494  volsup  25513  mbfss  25603  itg2cnlem2  25719  iblss2  25763  amgm  26957  wilthlem2  27035  ftalem3  27041  rpvmasum2  27479  noetasuplem4  27704  noetainflem4  27708  esumpad  34212  srcmpltd  35236  imadifss  37796  elrfi  42946  oaun2  43633  oaun3  43634  meaunle  46718  dfclnbgr4  48080  clnbupgr  48089