Theorem undif2 4457

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

Syntax hints:   = wceq 1540   ∖ cdif 3928   ∪ cun 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314

This theorem is referenced by:  undif  4462  dfif5  4522  funiunfv  7245  difex2  7759  undom  9078  undomOLD  9079  sucdom2OLD  9101  domss2  9155  sucdom2  9222  marypha1lem  9450  kmlem11  10180  hashun2  14406  hashun3  14407  cvgcmpce  15839  dprd2da  20030  dpjcntz  20040  dpjdisj  20041  dpjlsm  20042  dpjidcl  20046  ablfac1eu  20061  dfconn2  23362  2ndcdisj2  23400  fixufil  23865  fin1aufil  23875  xrge0gsumle  24778  unmbl  25495  volsup  25514  mbfss  25604  itg2cnlem2  25720  iblss2  25764  amgm  26958  wilthlem2  27036  ftalem3  27042  rpvmasum2  27480  noetasuplem4  27705  noetainflem4  27709  esumpad  34091  srcmpltd  35116  imadifss  37624  elrfi  42684  oaun2  43372  oaun3  43373  meaunle  46460  dfclnbgr4  47805  clnbupgr  47814