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  17580  lbsextlem4  21047  ufprim  23772  volun  25422  i1f1  25567  itgioo  25693  itgsplitioo  25715  plyeq0lem  26091  jensen  26875  difeq  32420  fzdif2  32686  fzodif2  32687  pmtrcnel2  33020  measun  34174  carsgclctunlem1  34281  carsggect  34282  chtvalz  34593  elmrsubrn  35480  mrsubvrs  35482  pibt2  37378  finixpnum  37572  lindsadd  37580  lindsenlbs  37582  poimirlem2  37589  poimirlem4  37591  poimirlem6  37593  poimirlem7  37594  poimirlem8  37595  poimirlem11  37598  poimirlem12  37599  poimirlem13  37600  poimirlem14  37601  poimirlem16  37603  poimirlem18  37605  poimirlem19  37606  poimirlem21  37608  poimirlem23  37610  poimirlem27  37614  poimirlem30  37617  asindmre  37670  disjresundif  38204  kelac2  43027  pwfi2f1o  43058  iccdifioo  45486  iccdifprioo  45487  hoiprodp1  46559