Theorem difun2 4436

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 4235	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4324	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4163	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4343	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2787	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

This proof depends on syntax axioms:   = wceq 1569   ∖ cdif 4044   ∪ cun 4148  ∅c0 4277

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278

This theorem is used by:  undif5  4439  uneqdifeq  4447  difprsn1  4759  orddif  6464  domunsncan  9104  elfiun  9429  hartogslem1  9543  cantnfp1lem3  9688  dju1dif  10258  infdju1  10275  ssxr  11386  dfn2  12626  incexclem  16014  mreexmrid  17826  lbsextlem4  21448  lindsenlbs  22166  ufprim  24237  volun  25875  i1f1  26020  itgioo  26145  itgsplitioo  26167  plyeq0lem  26538  jensen  27325  difeq  33165  fzdif2  33432  fzodif2  33433  pmtrcnel2  33701  measun  34894  carsgclctunlem1  34999  carsggect  35000  chtvalz  35308  elmrsubrn  36403  mrsubvrs  36405  pibt2  38477  finixpnum  38665  lindsadd  38673  poimirlem2  38677  poimirlem4  38679  poimirlem6  38681  poimirlem7  38682  poimirlem8  38683  poimirlem11  38686  poimirlem12  38687  poimirlem13  38688  poimirlem14  38689  poimirlem16  38691  poimirlem18  38693  poimirlem19  38694  poimirlem21  38696  poimirlem23  38698  poimirlem27  38702  poimirlem30  38705  asindmre  38758  disjresundif  39315  kelac2  44204  pwfi2f1o  44235  iccdifioo  46663  iccdifprioo  46664  hoiprodp1  47734