Theorem difun2 4244

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 4082	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4149	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 3963	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4165	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2832	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1637   ∖ cdif 3766   ∪ cun 3767  ∅c0 4116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117

This theorem is referenced by:  uneqdifeq  4253  difprsn1  4521  orddif  6030  domunsncan  8295  elfiun  8571  hartogslem1  8682  cantnfp1lem3  8820  cda1dif  9279  infcda1  9296  ssxr  10388  dfn2  11568  incexclem  14786  mreexmrid  16504  lbsextlem4  19366  ufprim  21923  volun  23525  i1f1  23670  itgioo  23795  itgsplitioo  23817  plyeq0lem  24179  jensen  24928  difeq  29679  fzdif2  29877  fzodif2  29878  measun  30598  carsgclctunlem1  30703  carsggect  30704  chtvalz  31031  elmrsubrn  31738  mrsubvrs  31740  finixpnum  33705  lindsenlbs  33715  poimirlem2  33722  poimirlem4  33724  poimirlem6  33726  poimirlem7  33727  poimirlem8  33728  poimirlem11  33731  poimirlem12  33732  poimirlem13  33733  poimirlem14  33734  poimirlem16  33736  poimirlem18  33738  poimirlem19  33739  poimirlem21  33741  poimirlem23  33743  poimirlem27  33747  poimirlem30  33750  asindmre  33805  kelac2  38133  pwfi2f1o  38164  iccdifioo  40219  iccdifprioo  40220  hoiprodp1  41281