Theorem undif2 4443

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

Syntax hints:   = wceq 1567   ∖ cdif 3910   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295

This theorem is referenced by:  undif  4448  dfif5  4509  imadifssran  6203  funiunfv  7247  difex2  7758  undom  9052  domss2  9123  sucdom2  9186  marypha1lem  9392  kmlem11  10143  hashun2  14418  hashun3  14419  cvgcmpce  15869  dprd2da  20113  dpjcntz  20123  dpjdisj  20124  dpjlsm  20125  dpjidcl  20129  ablfac1eu  20144  dfconn2  23544  2ndcdisj2  23582  fixufil  24047  fin1aufil  24057  xrge0gsumle  24959  unmbl  25664  volsup  25683  mbfss  25773  itg2cnlem2  25889  iblss2  25933  amgm  27120  wilthlem2  27198  ftalem3  27204  rpvmasum2  27641  noetasuplem4  27865  noetainflem4  27869  esumpad  34389  srcmpltd  35412  imadifss  38133  elrfi  43316  oaun2  43999  oaun3  44000  meaunle  47069  dfclnbgr4  48477  clnbupgr  48486