Theorem difun2 4422

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 4232	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4317	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4106	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4335	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2764	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1542   ∖ cdif 3887   ∪ cun 3888  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-nul 4275

This theorem is referenced by:  undif5  4425  uneqdifeq  4433  difprsn1  4744  orddif  6416  domunsncan  9009  elfiun  9337  hartogslem1  9451  cantnfp1lem3  9595  dju1dif  10089  infdju1  10106  ssxr  11209  dfn2  12444  incexclem  15795  mreexmrid  17603  lbsextlem4  21154  ufprim  23887  volun  25525  i1f1  25670  itgioo  25796  itgsplitioo  25818  plyeq0lem  26188  jensen  26969  difeq  32606  fzdif2  32881  fzodif2  32882  pmtrcnel2  33169  measun  34374  carsgclctunlem1  34480  carsggect  34481  chtvalz  34792  elmrsubrn  35721  mrsubvrs  35723  pibt2  37750  finixpnum  37943  lindsadd  37951  lindsenlbs  37953  poimirlem2  37960  poimirlem4  37962  poimirlem6  37964  poimirlem7  37965  poimirlem8  37966  poimirlem11  37969  poimirlem12  37970  poimirlem13  37971  poimirlem14  37972  poimirlem16  37974  poimirlem18  37976  poimirlem19  37977  poimirlem21  37979  poimirlem23  37981  poimirlem27  37985  poimirlem30  37988  asindmre  38041  disjresundif  38584  kelac2  43514  pwfi2f1o  43545  iccdifioo  45966  iccdifprioo  45967  hoiprodp1  47037