Theorem difun2 4504

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 4310	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4398	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4188	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4417	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2772	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1537   ∖ cdif 3973   ∪ cun 3974  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-nul 4353

This theorem is referenced by:  undif5  4508  uneqdifeq  4516  difprsn1  4825  orddif  6491  domunsncan  9138  elfiun  9499  hartogslem1  9611  cantnfp1lem3  9749  dju1dif  10242  infdju1  10259  ssxr  11359  dfn2  12566  incexclem  15884  mreexmrid  17701  lbsextlem4  21186  ufprim  23938  volun  25599  i1f1  25744  itgioo  25871  itgsplitioo  25893  plyeq0lem  26269  jensen  27050  difeq  32548  fzdif2  32796  fzodif2  32797  pmtrcnel2  33083  measun  34175  carsgclctunlem1  34282  carsggect  34283  chtvalz  34606  elmrsubrn  35488  mrsubvrs  35490  pibt2  37383  finixpnum  37565  lindsadd  37573  lindsenlbs  37575  poimirlem2  37582  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem16  37596  poimirlem18  37598  poimirlem19  37599  poimirlem21  37601  poimirlem23  37603  poimirlem27  37607  poimirlem30  37610  asindmre  37663  disjresundif  38198  kelac2  43022  pwfi2f1o  43053  iccdifioo  45433  iccdifprioo  45434  hoiprodp1  46509