Theorem undif2 4434

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3899   ∪ cun 3900

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283

This theorem is used by:  srcmpltd  4435  undif  4441  dfif5  4502  imadifssran  6201  funiunfv  7249  difex2  7763  undom  9067  domss2  9138  sucdom2  9201  marypha1lem  9407  kmlem11  10167  hashun2  14451  hashun3  14452  cvgcmpce  15909  dprd2da  20177  dpjcntz  20187  dpjdisj  20188  dpjlsm  20189  dpjidcl  20193  ablfac1eu  20208  dfconn2  23650  2ndcdisj2  23689  fixufil  24154  fin1aufil  24164  xrge0gsumle  25066  unmbl  25771  volsup  25790  mbfss  25880  itg2cnlem2  25996  iblss2  26040  amgm  27235  wilthlem2  27313  ftalem3  27319  rpvmasum2  27756  noetasuplem4  27980  noetainflem4  27984  esumpad  34573  imadifss  38362  elrfi  43547  oaun2  44230  oaun3  44231  meaunle  47300  dfclnbgr4  48748  clnbupgr  48757