Theorem difun2 4428

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 4238	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4323	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4112	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4341	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2758	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1541   ∖ cdif 3894   ∪ cun 3895  ∅c0 4280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-nul 4281

This theorem is referenced by:  undif5  4432  uneqdifeq  4440  difprsn1  4749  orddif  6404  domunsncan  8990  elfiun  9314  hartogslem1  9428  cantnfp1lem3  9570  dju1dif  10064  infdju1  10081  ssxr  11182  dfn2  12394  incexclem  15743  mreexmrid  17549  lbsextlem4  21098  ufprim  23824  volun  25473  i1f1  25618  itgioo  25744  itgsplitioo  25766  plyeq0lem  26142  jensen  26926  difeq  32498  fzdif2  32773  fzodif2  32774  pmtrcnel2  33059  measun  34224  carsgclctunlem1  34330  carsggect  34331  chtvalz  34642  elmrsubrn  35564  mrsubvrs  35566  pibt2  37461  finixpnum  37655  lindsadd  37663  lindsenlbs  37665  poimirlem2  37672  poimirlem4  37674  poimirlem6  37676  poimirlem7  37677  poimirlem8  37678  poimirlem11  37681  poimirlem12  37682  poimirlem13  37683  poimirlem14  37684  poimirlem16  37686  poimirlem18  37688  poimirlem19  37689  poimirlem21  37691  poimirlem23  37693  poimirlem27  37697  poimirlem30  37700  asindmre  37753  disjresundif  38291  kelac2  43168  pwfi2f1o  43199  iccdifioo  45625  iccdifprioo  45626  hoiprodp1  46696