Theorem undif2 4477

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

Syntax hints:   = wceq 1542   ∖ cdif 3946   ∪ cun 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324

This theorem is referenced by:  undif  4482  dfif5  4545  funiunfv  7247  difex2  7747  undom  9059  undomOLD  9060  sucdom2OLD  9082  domss2  9136  sucdom2  9206  unfiOLD  9313  marypha1lem  9428  kmlem11  10155  hashun2  14343  hashun3  14344  cvgcmpce  15764  dprd2da  19912  dpjcntz  19922  dpjdisj  19923  dpjlsm  19924  dpjidcl  19928  ablfac1eu  19943  dfconn2  22923  2ndcdisj2  22961  fixufil  23426  fin1aufil  23436  xrge0gsumle  24349  unmbl  25054  volsup  25073  mbfss  25163  itg2cnlem2  25280  iblss2  25323  amgm  26495  wilthlem2  26573  ftalem3  26579  rpvmasum2  27015  noetasuplem4  27239  noetainflem4  27243  esumpad  33084  srcmpltd  34116  imadifss  36511  elrfi  41480  oaun2  42179  oaun3  42180  meaunle  45228