Theorem undif2 4430

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

This proof depends on syntax axioms:   = wceq 1569   ∖ cdif 4044   ∪ cun 4148

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278

This theorem is used by:  srcmpltd  4431  undif  4437  dfif5  4498  imadifssranOLD  6205  funiunfv  7256  difex2  7778  undom  9092  domss2  9163  sucdom2  9226  marypha1lem  9432  kmlem11  10246  hashun2  14534  hashun3  14535  cvgcmpce  15994  dprd2da  20267  dpjcntz  20277  dpjdisj  20278  dpjlsm  20279  dpjidcl  20283  ablfac1eu  20298  dfconn2  23746  2ndcdisj2  23785  fixufil  24250  fin1aufil  24260  xrge0gsumle  25162  unmbl  25867  volsup  25886  mbfss  25976  itg2cnlem2  26092  iblss2  26135  amgm  27327  wilthlem2  27405  ftalem3  27411  rpvmasum2  27848  noetasuplem4  28102  noetainflem4  28106  esumpad  34737  imadifss  38660  elrfi  43842  oaun2  44520  oaun3  44521  meaunle  47610  dfclnbgr4  49058  clnbupgr  49067