Theorem difun2 4307

Description: Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)

Assertion

Ref	Expression
difun2	⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Proof of Theorem difun2

Step	Hyp	Ref	Expression
1		difundir 4139	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4211	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4020	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4225	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2801	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1508   ∖ cdif 3821   ∪ cun 3822  ∅c0 4173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ral 3088  df-rab 3092  df-v 3412  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174

This theorem is referenced by:  uneqdifeq  4316  difprsn1  4604  orddif  6120  domunsncan  8412  elfiun  8688  hartogslem1  8800  cantnfp1lem3  8936  dju1dif  9395  infdju1  9412  ssxr  10509  dfn2  11721  incexclem  15050  mreexmrid  16785  lbsextlem4  19668  ufprim  22237  volun  23865  i1f1  24010  itgioo  24135  itgsplitioo  24157  plyeq0lem  24519  jensen  25284  difeq  30072  fzdif2  30289  fzodif2  30290  measun  31148  carsgclctunlem1  31253  carsggect  31254  chtvalz  31581  elmrsubrn  32320  mrsubvrs  32322  pibt2  34172  finixpnum  34351  lindsadd  34359  lindsenlbs  34361  poimirlem2  34368  poimirlem4  34370  poimirlem6  34372  poimirlem7  34373  poimirlem8  34374  poimirlem11  34377  poimirlem12  34378  poimirlem13  34379  poimirlem14  34380  poimirlem16  34382  poimirlem18  34384  poimirlem19  34385  poimirlem21  34387  poimirlem23  34389  poimirlem27  34393  poimirlem30  34396  asindmre  34451  kelac2  39095  pwfi2f1o  39126  iccdifioo  41252  iccdifprioo  41253  hoiprodp1  42331