Theorem undif2 4425

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

Syntax hints:   = wceq 1537   ∖ cdif 3933   ∪ cun 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292

This theorem is referenced by:  undif  4430  dfif5  4483  funiunfv  7007  difex2  7482  undom  8605  domss2  8676  sucdom2  8714  unfi  8785  marypha1lem  8897  kmlem11  9586  hashun2  13745  hashun3  13746  cvgcmpce  15173  dprd2da  19164  dpjcntz  19174  dpjdisj  19175  dpjlsm  19176  dpjidcl  19180  ablfac1eu  19195  dfconn2  22027  2ndcdisj2  22065  fixufil  22530  fin1aufil  22540  xrge0gsumle  23441  unmbl  24138  volsup  24157  mbfss  24247  itg2cnlem2  24363  iblss2  24406  amgm  25568  wilthlem2  25646  ftalem3  25652  rpvmasum2  26088  esumpad  31314  srcmpltd  32346  noetalem3  33219  noetalem4  33220  imadifss  34882  elrfi  39311  meaunle  42766