Theorem undif2 4405

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

Syntax hints:   = wceq 1547   ∖ cdif 3880   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262

This theorem is referenced by:  undif  4410  dfif5  4471  funiunfv  7192  difex2  7703  undom  8993  domss2  9064  sucdom2  9127  marypha1lem  9336  kmlem11  10074  hashun2  14336  hashun3  14337  cvgcmpce  15772  dprd2da  20010  dpjcntz  20020  dpjdisj  20021  dpjlsm  20022  dpjidcl  20026  ablfac1eu  20041  dfconn2  23402  2ndcdisj2  23440  fixufil  23905  fin1aufil  23915  xrge0gsumle  24817  unmbl  25522  volsup  25541  mbfss  25631  itg2cnlem2  25747  iblss2  25791  amgm  26972  wilthlem2  27050  ftalem3  27056  rpvmasum2  27493  noetasuplem4  27718  noetainflem4  27722  esumpad  34239  srcmpltd  35262  imadifss  37962  elrfi  43143  oaun2  43826  oaun3  43827  meaunle  46907  dfclnbgr4  48315  clnbupgr  48324