Theorem undif2 4431

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

Syntax hints:   = wceq 1560   ∖ cdif 3901   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286

This theorem is referenced by:  undif  4436  dfif5  4497  funiunfv  7232  difex2  7743  undom  9037  domss2  9108  sucdom2  9171  marypha1lem  9379  kmlem11  10117  hashun2  14396  hashun3  14397  cvgcmpce  15846  dprd2da  20084  dpjcntz  20094  dpjdisj  20095  dpjlsm  20096  dpjidcl  20100  ablfac1eu  20115  dfconn2  23479  2ndcdisj2  23517  fixufil  23982  fin1aufil  23992  xrge0gsumle  24894  unmbl  25599  volsup  25618  mbfss  25708  itg2cnlem2  25824  iblss2  25868  amgm  27055  wilthlem2  27133  ftalem3  27139  rpvmasum2  27576  noetasuplem4  27800  noetainflem4  27804  esumpad  34352  srcmpltd  35375  imadifss  38094  elrfi  43275  oaun2  43958  oaun3  43959  meaunle  47038  dfclnbgr4  48446  clnbupgr  48455