Theorem difun2 4440

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 4250	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4335	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4124	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4353	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2756	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1540   ∖ cdif 3908   ∪ cun 3909  ∅c0 4292

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-nul 4293

This theorem is referenced by:  undif5  4444  uneqdifeq  4452  difprsn1  4760  orddif  6418  domunsncan  9018  elfiun  9357  hartogslem1  9471  cantnfp1lem3  9609  dju1dif  10102  infdju1  10119  ssxr  11219  dfn2  12431  incexclem  15778  mreexmrid  17584  lbsextlem4  21103  ufprim  23829  volun  25479  i1f1  25624  itgioo  25750  itgsplitioo  25772  plyeq0lem  26148  jensen  26932  difeq  32497  fzdif2  32763  fzodif2  32764  pmtrcnel2  33062  measun  34194  carsgclctunlem1  34301  carsggect  34302  chtvalz  34613  elmrsubrn  35500  mrsubvrs  35502  pibt2  37398  finixpnum  37592  lindsadd  37600  lindsenlbs  37602  poimirlem2  37609  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem11  37618  poimirlem12  37619  poimirlem13  37620  poimirlem14  37621  poimirlem16  37623  poimirlem18  37625  poimirlem19  37626  poimirlem21  37628  poimirlem23  37630  poimirlem27  37634  poimirlem30  37637  asindmre  37690  disjresundif  38224  kelac2  43047  pwfi2f1o  43078  iccdifioo  45506  iccdifprioo  45507  hoiprodp1  46579