Theorem undif2 4268

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

Syntax hints:   = wceq 1601   ∖ cdif 3789   ∪ cun 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142

This theorem is referenced by:  undif  4273  dfif5  4323  funiunfv  6780  difex2  7248  undom  8338  domss2  8409  sucdom2  8446  unfi  8517  marypha1lem  8629  kmlem11  9319  hashun2  13491  hashun3  13492  cvgcmpce  14958  dprd2da  18832  dpjcntz  18842  dpjdisj  18843  dpjlsm  18844  dpjidcl  18848  ablfac1eu  18863  dfconn2  21635  2ndcdisj2  21673  fixufil  22138  fin1aufil  22148  xrge0gsumle  23048  unmbl  23745  volsup  23764  mbfss  23854  itg2cnlem2  23970  iblss2  24013  amgm  25173  wilthlem2  25251  ftalem3  25257  rpvmasum2  25657  esumpad  30719  noetalem3  32458  noetalem4  32459  imadifss  34014  elrfi  38227  meaunle  41615