Theorem undif2 4383

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

Syntax hints:   = wceq 1538   ∖ cdif 3878   ∪ cun 3879

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244

This theorem is referenced by:  undif  4388  dfif5  4441  funiunfv  6985  difex2  7462  undom  8588  sucdom2  8610  domss2  8660  unfi  8769  marypha1lem  8881  kmlem11  9571  hashun2  13740  hashun3  13741  cvgcmpce  15165  dprd2da  19157  dpjcntz  19167  dpjdisj  19168  dpjlsm  19169  dpjidcl  19173  ablfac1eu  19188  dfconn2  22024  2ndcdisj2  22062  fixufil  22527  fin1aufil  22537  xrge0gsumle  23438  unmbl  24141  volsup  24160  mbfss  24250  itg2cnlem2  24366  iblss2  24409  amgm  25576  wilthlem2  25654  ftalem3  25660  rpvmasum2  26096  esumpad  31424  srcmpltd  32456  noetalem3  33332  noetalem4  33333  imadifss  35032  elrfi  39635  meaunle  43103