Theorem difun2 4480

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 4290	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4375	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4164	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4393	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2768	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1539   ∖ cdif 3947   ∪ cun 3948  ∅c0 4332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-nul 4333

This theorem is referenced by:  undif5  4484  uneqdifeq  4492  difprsn1  4799  orddif  6479  domunsncan  9113  elfiun  9471  hartogslem1  9583  cantnfp1lem3  9721  dju1dif  10214  infdju1  10231  ssxr  11331  dfn2  12541  incexclem  15873  mreexmrid  17687  lbsextlem4  21164  ufprim  23918  volun  25581  i1f1  25726  itgioo  25852  itgsplitioo  25874  plyeq0lem  26250  jensen  27033  difeq  32538  fzdif2  32793  fzodif2  32794  pmtrcnel2  33111  measun  34213  carsgclctunlem1  34320  carsggect  34321  chtvalz  34645  elmrsubrn  35526  mrsubvrs  35528  pibt2  37419  finixpnum  37613  lindsadd  37621  lindsenlbs  37623  poimirlem2  37630  poimirlem4  37632  poimirlem6  37634  poimirlem7  37635  poimirlem8  37636  poimirlem11  37639  poimirlem12  37640  poimirlem13  37641  poimirlem14  37642  poimirlem16  37644  poimirlem18  37646  poimirlem19  37647  poimirlem21  37649  poimirlem23  37651  poimirlem27  37655  poimirlem30  37658  asindmre  37711  disjresundif  38245  kelac2  43082  pwfi2f1o  43113  iccdifioo  45533  iccdifprioo  45534  hoiprodp1  46608