Theorem undif2 4431

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3896   ∪ cun 3897

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280

This theorem is used by:  srcmpltd  4432  undif  4438  dfif5  4499  imadifssran  6197  funiunfv  7246  difex2  7760  undom  9064  domss2  9135  sucdom2  9198  marypha1lem  9404  kmlem11  10164  hashun2  14448  hashun3  14449  cvgcmpce  15906  dprd2da  20172  dpjcntz  20182  dpjdisj  20183  dpjlsm  20184  dpjidcl  20188  ablfac1eu  20203  dfconn2  23645  2ndcdisj2  23684  fixufil  24149  fin1aufil  24159  xrge0gsumle  25061  unmbl  25766  volsup  25785  mbfss  25875  itg2cnlem2  25991  iblss2  26034  amgm  27228  wilthlem2  27306  ftalem3  27312  rpvmasum2  27749  noetasuplem4  27973  noetainflem4  27977  esumpad  34566  imadifss  38355  elrfi  43540  oaun2  44223  oaun3  44224  meaunle  47293  dfclnbgr4  48741  clnbupgr  48750