Theorem undif2 4016

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

Syntax hints:   = wceq 1480   ∖ cdif 3552   ∪ cun 3553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892

This theorem is referenced by:  undif  4021  dfif5  4074  funiunfv  6460  difex2  6918  undom  7992  domss2  8063  sucdom2  8100  unfi  8171  marypha1lem  8283  kmlem11  8926  hashun2  13112  hashun3  13113  cvgcmpce  14477  dprd2da  18362  dpjcntz  18372  dpjdisj  18373  dpjlsm  18374  dpjidcl  18378  ablfac1eu  18393  dfconn2  21132  2ndcdisj2  21170  fixufil  21636  fin1aufil  21646  xrge0gsumle  22544  unmbl  23212  volsup  23231  mbfss  23319  itg2cnlem2  23435  iblss2  23478  amgm  24617  wilthlem2  24695  ftalem3  24701  rpvmasum2  25101  esumpad  29898  imadifss  33016  elrfi  36737  meaunle  39988