Theorem undif2 4431

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3896   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280

This theorem is used by:  srcmpltd  4432  undif  4438  dfif5  4499  imadifssranOLD  6202  funiunfv  7252  difex2  7774  undom  9084  domss2  9155  sucdom2  9218  marypha1lem  9425  kmlem11  10239  hashun2  14527  hashun3  14528  cvgcmpce  15985  dprd2da  20258  dpjcntz  20268  dpjdisj  20269  dpjlsm  20270  dpjidcl  20274  ablfac1eu  20289  dfconn2  23737  2ndcdisj2  23776  fixufil  24241  fin1aufil  24251  xrge0gsumle  25153  unmbl  25858  volsup  25877  mbfss  25967  itg2cnlem2  26083  iblss2  26126  amgm  27318  wilthlem2  27396  ftalem3  27402  rpvmasum2  27839  noetasuplem4  28093  noetainflem4  28097  esumpad  34687  imadifss  38523  elrfi  43704  oaun2  44382  oaun3  44383  meaunle  47473  dfclnbgr4  48921  clnbupgr  48930