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 4160	. 2 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∪ 𝐴)
2		undif1 4433	. 2 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴)
3		uncom 4160	. 2 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵)
4	1, 2, 3	3eqtri 2790	1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 4048   ∪ cun 4152

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282

This theorem is used by:  srcmpltd  4435  undif  4441  dfif5  4502  imadifssranOLD  6221  funiunfv  7283  difex2  7806  undom  9122  domss2  9193  sucdom2  9256  marypha1lem  9462  kmlem11  10278  hashun2  14568  hashun3  14569  cvgcmpce  16029  dprd2da  20309  dpjcntz  20319  dpjdisj  20320  dpjlsm  20321  dpjidcl  20325  ablfac1eu  20340  dfconn2  23792  2ndcdisj2  23831  fixufil  24296  fin1aufil  24306  xrge0gsumle  25208  unmbl  25913  volsup  25932  mbfss  26022  itg2cnlem2  26138  iblss2  26181  amgm  27375  wilthlem2  27453  ftalem3  27459  rpvmasum2  27896  noetasuplem4  28150  noetainflem4  28154  esumpad  34798  imadifss  38791  elrfi  43971  oaun2  44644  oaun3  44645  meaunle  47747  dfclnbgr4  49195  clnbupgr  49204