Theorem undif2 4427

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

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

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284

This theorem is referenced by:  undif  4432  dfif5  4494  funiunfv  7192  difex2  7703  undom  8991  domss2  9062  sucdom2  9125  marypha1lem  9334  kmlem11  10069  hashun2  14304  hashun3  14305  cvgcmpce  15739  dprd2da  19971  dpjcntz  19981  dpjdisj  19982  dpjlsm  19983  dpjidcl  19987  ablfac1eu  20002  dfconn2  23361  2ndcdisj2  23399  fixufil  23864  fin1aufil  23874  xrge0gsumle  24776  unmbl  25492  volsup  25511  mbfss  25601  itg2cnlem2  25717  iblss2  25761  amgm  26955  wilthlem2  27033  ftalem3  27039  rpvmasum2  27477  noetasuplem4  27702  noetainflem4  27706  esumpad  34161  srcmpltd  35185  imadifss  37735  elrfi  42878  oaun2  43565  oaun3  43566  meaunle  46650  dfclnbgr4  48012  clnbupgr  48021