Theorem undif2 4440

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

Syntax hints:   = wceq 1540   ∖ cdif 3911   ∪ cun 3912

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297

This theorem is referenced by:  undif  4445  dfif5  4505  funiunfv  7222  difex2  7736  undom  9029  domss2  9100  sucdom2  9167  marypha1lem  9384  kmlem11  10114  hashun2  14348  hashun3  14349  cvgcmpce  15784  dprd2da  19974  dpjcntz  19984  dpjdisj  19985  dpjlsm  19986  dpjidcl  19990  ablfac1eu  20005  dfconn2  23306  2ndcdisj2  23344  fixufil  23809  fin1aufil  23819  xrge0gsumle  24722  unmbl  25438  volsup  25457  mbfss  25547  itg2cnlem2  25663  iblss2  25707  amgm  26901  wilthlem2  26979  ftalem3  26985  rpvmasum2  27423  noetasuplem4  27648  noetainflem4  27652  esumpad  34045  srcmpltd  35070  imadifss  37589  elrfi  42682  oaun2  43370  oaun3  43371  meaunle  46462  dfclnbgr4  47825  clnbupgr  47834