Theorem difun2 4485

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 4282	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4375	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4160	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4395	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2758	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1534   ∖ cdif 3944   ∪ cun 3945  ∅c0 4325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-nul 4326

This theorem is referenced by:  undif5  4489  uneqdifeq  4497  difprsn1  4809  orddif  6472  domunsncan  9110  elfiun  9473  hartogslem1  9585  cantnfp1lem3  9723  dju1dif  10215  infdju1  10232  ssxr  11333  dfn2  12537  incexclem  15840  mreexmrid  17656  lbsextlem4  21142  ufprim  23904  volun  25565  i1f1  25710  itgioo  25836  itgsplitioo  25858  plyeq0lem  26237  jensen  27017  difeq  32445  fzdif2  32693  fzodif2  32694  pmtrcnel2  32968  measun  34044  carsgclctunlem1  34151  carsggect  34152  chtvalz  34475  elmrsubrn  35348  mrsubvrs  35350  pibt2  37124  finixpnum  37306  lindsadd  37314  lindsenlbs  37316  poimirlem2  37323  poimirlem4  37325  poimirlem6  37327  poimirlem7  37328  poimirlem8  37329  poimirlem11  37332  poimirlem12  37333  poimirlem13  37334  poimirlem14  37335  poimirlem16  37337  poimirlem18  37339  poimirlem19  37340  poimirlem21  37342  poimirlem23  37344  poimirlem27  37348  poimirlem30  37351  asindmre  37404  disjresundif  37940  kelac2  42726  pwfi2f1o  42757  iccdifioo  45133  iccdifprioo  45134  hoiprodp1  46209