Theorem undif2 4416

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

Syntax hints:   = wceq 1542   ∖ cdif 3889   ∪ cun 3890

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263

This theorem is referenced by:  undif  4421  dfif5  4481  funiunfv  7116  difex2  7602  undom  8821  sucdom2  8843  domss2  8897  unfiOLD  9051  marypha1lem  9162  kmlem11  9909  hashun2  14088  hashun3  14089  cvgcmpce  15520  dprd2da  19635  dpjcntz  19645  dpjdisj  19646  dpjlsm  19647  dpjidcl  19651  ablfac1eu  19666  dfconn2  22560  2ndcdisj2  22598  fixufil  23063  fin1aufil  23073  xrge0gsumle  23986  unmbl  24691  volsup  24710  mbfss  24800  itg2cnlem2  24917  iblss2  24960  amgm  26130  wilthlem2  26208  ftalem3  26214  rpvmasum2  26650  esumpad  32011  srcmpltd  33042  noetasuplem4  33927  noetainflem4  33931  imadifss  35740  elrfi  40505  meaunle  43965