Theorem undif2 4417

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

Syntax hints:   = wceq 1542   ∖ cdif 3886   ∪ cun 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274

This theorem is referenced by:  undif  4422  dfif5  4483  funiunfv  7203  difex2  7714  undom  9003  domss2  9074  sucdom2  9137  marypha1lem  9346  kmlem11  10083  hashun2  14345  hashun3  14346  cvgcmpce  15781  dprd2da  20019  dpjcntz  20029  dpjdisj  20030  dpjlsm  20031  dpjidcl  20035  ablfac1eu  20050  dfconn2  23384  2ndcdisj2  23422  fixufil  23887  fin1aufil  23897  xrge0gsumle  24799  unmbl  25504  volsup  25523  mbfss  25613  itg2cnlem2  25729  iblss2  25773  amgm  26954  wilthlem2  27032  ftalem3  27038  rpvmasum2  27475  noetasuplem4  27700  noetainflem4  27704  esumpad  34199  srcmpltd  35222  imadifss  37916  elrfi  43126  oaun2  43809  oaun3  43810  meaunle  46892  dfclnbgr4  48300  clnbupgr  48309