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 4243	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4329	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4118	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4348	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2789	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1560   ∖ cdif 3901   ∪ cun 3902  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-nul 4286

This theorem is referenced by:  undif5  4438  uneqdifeq  4446  difprsn1  4760  orddif  6444  domunsncan  9049  elfiun  9376  hartogslem1  9490  cantnfp1lem3  9635  dju1dif  10129  infdju1  10146  ssxr  11252  dfn2  12494  incexclem  15866  mreexmrid  17675  lbsextlem4  21231  ufprim  23969  volun  25607  i1f1  25752  itgioo  25878  itgsplitioo  25900  plyeq0lem  26270  jensen  27053  difeq  32717  fzdif2  32992  fzodif2  32993  pmtrcnel2  33270  measun  34508  carsgclctunlem1  34614  carsggect  34615  chtvalz  34923  elmrsubrn  35870  mrsubvrs  35872  pibt2  37911  finixpnum  38104  lindsadd  38112  lindsenlbs  38114  poimirlem2  38121  poimirlem4  38123  poimirlem6  38125  poimirlem7  38126  poimirlem8  38127  poimirlem11  38130  poimirlem12  38131  poimirlem13  38132  poimirlem14  38133  poimirlem16  38135  poimirlem18  38137  poimirlem19  38138  poimirlem21  38140  poimirlem23  38142  poimirlem27  38146  poimirlem30  38149  asindmre  38202  disjresundif  38745  kelac2  43642  pwfi2f1o  43673  iccdifioo  46091  iccdifprioo  46092  hoiprodp1  47162