Theorem difun2 4414

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 4214	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4304	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4094	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4324	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2770	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1539   ∖ cdif 3884   ∪ cun 3885  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-nul 4257

This theorem is referenced by:  uneqdifeq  4423  difprsn1  4733  orddif  6359  domunsncan  8859  elfiun  9189  hartogslem1  9301  cantnfp1lem3  9438  dju1dif  9928  infdju1  9945  ssxr  11044  dfn2  12246  incexclem  15548  mreexmrid  17352  lbsextlem4  20423  ufprim  23060  volun  24709  i1f1  24854  itgioo  24980  itgsplitioo  25002  plyeq0lem  25371  jensen  26138  difeq  30865  undif5  30867  fzdif2  31112  fzodif2  31113  pmtrcnel2  31359  measun  32179  carsgclctunlem1  32284  carsggect  32285  chtvalz  32609  elmrsubrn  33482  mrsubvrs  33484  pibt2  35588  finixpnum  35762  lindsadd  35770  lindsenlbs  35772  poimirlem2  35779  poimirlem4  35781  poimirlem6  35783  poimirlem7  35784  poimirlem8  35785  poimirlem11  35788  poimirlem12  35789  poimirlem13  35790  poimirlem14  35791  poimirlem16  35793  poimirlem18  35795  poimirlem19  35796  poimirlem21  35798  poimirlem23  35800  poimirlem27  35804  poimirlem30  35807  asindmre  35860  kelac2  40890  pwfi2f1o  40921  iccdifioo  43053  iccdifprioo  43054  hoiprodp1  44126