Theorem difun2 4461

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 4271	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4356	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4145	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4374	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2763	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1540   ∖ cdif 3928   ∪ cun 3929  ∅c0 4313

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-nul 4314

This theorem is referenced by:  undif5  4465  uneqdifeq  4473  difprsn1  4781  orddif  6455  domunsncan  9091  elfiun  9447  hartogslem1  9561  cantnfp1lem3  9699  dju1dif  10192  infdju1  10209  ssxr  11309  dfn2  12519  incexclem  15857  mreexmrid  17660  lbsextlem4  21127  ufprim  23852  volun  25503  i1f1  25648  itgioo  25774  itgsplitioo  25796  plyeq0lem  26172  jensen  26956  difeq  32504  fzdif2  32772  fzodif2  32773  pmtrcnel2  33106  measun  34247  carsgclctunlem1  34354  carsggect  34355  chtvalz  34666  elmrsubrn  35547  mrsubvrs  35549  pibt2  37440  finixpnum  37634  lindsadd  37642  lindsenlbs  37644  poimirlem2  37651  poimirlem4  37653  poimirlem6  37655  poimirlem7  37656  poimirlem8  37657  poimirlem11  37660  poimirlem12  37661  poimirlem13  37662  poimirlem14  37663  poimirlem16  37665  poimirlem18  37667  poimirlem19  37668  poimirlem21  37670  poimirlem23  37672  poimirlem27  37676  poimirlem30  37679  asindmre  37732  disjresundif  38266  kelac2  43056  pwfi2f1o  43087  iccdifioo  45511  iccdifprioo  45512  hoiprodp1  46584