Theorem difun2 4435

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 4245	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4330	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4119	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4348	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2764	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1542   ∖ cdif 3900   ∪ cun 3901  ∅c0 4287

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-nul 4288

This theorem is referenced by:  undif5  4439  uneqdifeq  4447  difprsn1  4758  orddif  6423  domunsncan  9017  elfiun  9345  hartogslem1  9459  cantnfp1lem3  9601  dju1dif  10095  infdju1  10112  ssxr  11214  dfn2  12426  incexclem  15771  mreexmrid  17578  lbsextlem4  21128  ufprim  23865  volun  25514  i1f1  25659  itgioo  25785  itgsplitioo  25807  plyeq0lem  26183  jensen  26967  difeq  32605  fzdif2  32881  fzodif2  32882  pmtrcnel2  33184  measun  34389  carsgclctunlem1  34495  carsggect  34496  chtvalz  34807  elmrsubrn  35736  mrsubvrs  35738  pibt2  37672  finixpnum  37856  lindsadd  37864  lindsenlbs  37866  poimirlem2  37873  poimirlem4  37875  poimirlem6  37877  poimirlem7  37878  poimirlem8  37879  poimirlem11  37882  poimirlem12  37883  poimirlem13  37884  poimirlem14  37885  poimirlem16  37887  poimirlem18  37889  poimirlem19  37890  poimirlem21  37892  poimirlem23  37894  poimirlem27  37898  poimirlem30  37901  asindmre  37954  disjresundif  38497  kelac2  43422  pwfi2f1o  43453  iccdifioo  45875  iccdifprioo  45876  hoiprodp1  46946