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 2790	1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1570   ∖ cdif 3902   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287

This theorem is referenced by:  undif  4443  dfif5  4504  imadifssran  6202  funiunfv  7246  difex2  7755  undom  9049  domss2  9120  sucdom2  9183  marypha1lem  9389  kmlem11  10140  hashun2  14415  hashun3  14416  cvgcmpce  15866  dprd2da  20109  dpjcntz  20119  dpjdisj  20120  dpjlsm  20121  dpjidcl  20125  ablfac1eu  20140  dfconn2  23576  2ndcdisj2  23614  fixufil  24079  fin1aufil  24089  xrge0gsumle  24991  unmbl  25696  volsup  25715  mbfss  25805  itg2cnlem2  25921  iblss2  25965  amgm  27155  wilthlem2  27233  ftalem3  27239  rpvmasum2  27676  noetasuplem4  27900  noetainflem4  27904  esumpad  34445  srcmpltd  35469  imadifss  38246  elrfi  43425  oaun2  44108  oaun3  44109  meaunle  47178  dfclnbgr4  48589  clnbupgr  48598