Theorem undif2 4438

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3903   ∪ cun 3904

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287

This theorem is used by:  srcmpltd  4439  undif  4445  dfif5  4506  imadifssran  6204  funiunfv  7251  difex2  7765  undom  9060  domss2  9131  sucdom2  9194  marypha1lem  9400  kmlem11  10160  hashun2  14437  hashun3  14438  cvgcmpce  15893  dprd2da  20158  dpjcntz  20168  dpjdisj  20169  dpjlsm  20170  dpjidcl  20174  ablfac1eu  20189  dfconn2  23626  2ndcdisj2  23665  fixufil  24130  fin1aufil  24140  xrge0gsumle  25042  unmbl  25747  volsup  25766  mbfss  25856  itg2cnlem2  25972  iblss2  26016  amgm  27206  wilthlem2  27284  ftalem3  27290  rpvmasum2  27727  noetasuplem4  27951  noetainflem4  27955  esumpad  34509  imadifss  38303  elrfi  43483  oaun2  44166  oaun3  44167  meaunle  47236  dfclnbgr4  48647  clnbupgr  48656