Theorem undif2 4407

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254

This theorem is referenced by:  undif  4412  dfif5  4472  funiunfv  7103  difex2  7588  undom  8800  sucdom2  8822  domss2  8872  unfiOLD  9011  marypha1lem  9122  kmlem11  9847  hashun2  14026  hashun3  14027  cvgcmpce  15458  dprd2da  19560  dpjcntz  19570  dpjdisj  19571  dpjlsm  19572  dpjidcl  19576  ablfac1eu  19591  dfconn2  22478  2ndcdisj2  22516  fixufil  22981  fin1aufil  22991  xrge0gsumle  23902  unmbl  24606  volsup  24625  mbfss  24715  itg2cnlem2  24832  iblss2  24875  amgm  26045  wilthlem2  26123  ftalem3  26129  rpvmasum2  26565  esumpad  31923  srcmpltd  32954  noetasuplem4  33866  noetainflem4  33870  imadifss  35679  elrfi  40432  meaunle  43892