Theorem undif2 4424

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

Syntax hints:   = wceq 1533   ∖ cdif 3932   ∪ cun 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291

This theorem is referenced by:  undif  4429  dfif5  4482  funiunfv  7006  difex2  7481  undom  8604  domss2  8675  sucdom2  8713  unfi  8784  marypha1lem  8896  kmlem11  9585  hashun2  13743  hashun3  13744  cvgcmpce  15172  dprd2da  19163  dpjcntz  19173  dpjdisj  19174  dpjlsm  19175  dpjidcl  19179  ablfac1eu  19194  dfconn2  22026  2ndcdisj2  22064  fixufil  22529  fin1aufil  22539  xrge0gsumle  23440  unmbl  24137  volsup  24156  mbfss  24246  itg2cnlem2  24362  iblss2  24405  amgm  25567  wilthlem2  25645  ftalem3  25651  rpvmasum2  26087  esumpad  31314  srcmpltd  32346  noetalem3  33219  noetalem4  33220  imadifss  34866  elrfi  39289  meaunle  42745