Theorem difun2 4481

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 4281	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4371	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4161	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4391	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2762	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1539   ∖ cdif 3946   ∪ cun 3947  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-nul 4324

This theorem is referenced by:  undif5  4485  uneqdifeq  4493  difprsn1  4804  orddif  6461  domunsncan  9076  elfiun  9429  hartogslem1  9541  cantnfp1lem3  9679  dju1dif  10171  infdju1  10188  ssxr  11289  dfn2  12491  incexclem  15788  mreexmrid  17593  lbsextlem4  20921  ufprim  23635  volun  25296  i1f1  25441  itgioo  25567  itgsplitioo  25589  plyeq0lem  25958  jensen  26727  difeq  32021  fzdif2  32267  fzodif2  32268  pmtrcnel2  32519  measun  33505  carsgclctunlem1  33612  carsggect  33613  chtvalz  33937  elmrsubrn  34807  mrsubvrs  34809  pibt2  36603  finixpnum  36778  lindsadd  36786  lindsenlbs  36788  poimirlem2  36795  poimirlem4  36797  poimirlem6  36799  poimirlem7  36800  poimirlem8  36801  poimirlem11  36804  poimirlem12  36805  poimirlem13  36806  poimirlem14  36807  poimirlem16  36809  poimirlem18  36811  poimirlem19  36812  poimirlem21  36814  poimirlem23  36816  poimirlem27  36820  poimirlem30  36823  asindmre  36876  disjresundif  37414  kelac2  42111  pwfi2f1o  42142  iccdifioo  44528  iccdifprioo  44529  hoiprodp1  45604