Theorem difun2 4395

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 4195	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4285	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4074	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4305	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2769	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1543   ∖ cdif 3863   ∪ cun 3864  ∅c0 4237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-nul 4238

This theorem is referenced by:  uneqdifeq  4404  difprsn1  4713  orddif  6306  domunsncan  8745  elfiun  9046  hartogslem1  9158  cantnfp1lem3  9295  dju1dif  9786  infdju1  9803  ssxr  10902  dfn2  12103  incexclem  15400  mreexmrid  17146  lbsextlem4  20198  ufprim  22806  volun  24442  i1f1  24587  itgioo  24713  itgsplitioo  24735  plyeq0lem  25104  jensen  25871  difeq  30584  undif5  30586  fzdif2  30832  fzodif2  30833  pmtrcnel2  31078  measun  31891  carsgclctunlem1  31996  carsggect  31997  chtvalz  32321  elmrsubrn  33195  mrsubvrs  33197  pibt2  35325  finixpnum  35499  lindsadd  35507  lindsenlbs  35509  poimirlem2  35516  poimirlem4  35518  poimirlem6  35520  poimirlem7  35521  poimirlem8  35522  poimirlem11  35525  poimirlem12  35526  poimirlem13  35527  poimirlem14  35528  poimirlem16  35530  poimirlem18  35532  poimirlem19  35533  poimirlem21  35535  poimirlem23  35537  poimirlem27  35541  poimirlem30  35544  asindmre  35597  kelac2  40593  pwfi2f1o  40624  iccdifioo  42728  iccdifprioo  42729  hoiprodp1  43801