Theorem difun2 4442

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 4244	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4332	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4119	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4351	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2790	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1570   ∖ cdif 3902   ∪ cun 3903  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-nul 4287

This theorem is referenced by:  undif5  4445  uneqdifeq  4453  difprsn1  4768  orddif  6459  domunsncan  9061  elfiun  9386  hartogslem1  9500  cantnfp1lem3  9645  dju1dif  10152  infdju1  10169  ssxr  11274  dfn2  12512  incexclem  15886  mreexmrid  17694  lbsextlem4  21285  ufprim  24066  volun  25704  i1f1  25849  itgioo  25975  itgsplitioo  25997  plyeq0lem  26367  jensen  27153  difeq  32864  fzdif2  33135  fzodif2  33136  pmtrcnel2  33410  measun  34601  carsgclctunlem1  34707  carsggect  34708  chtvalz  35016  elmrsubrn  36012  mrsubvrs  36014  pibt2  38063  finixpnum  38256  lindsadd  38264  lindsenlbs  38266  poimirlem2  38273  poimirlem4  38275  poimirlem6  38277  poimirlem7  38278  poimirlem8  38279  poimirlem11  38282  poimirlem12  38283  poimirlem13  38284  poimirlem14  38285  poimirlem16  38287  poimirlem18  38289  poimirlem19  38290  poimirlem21  38292  poimirlem23  38294  poimirlem27  38298  poimirlem30  38301  asindmre  38354  disjresundif  38895  kelac2  43792  pwfi2f1o  43823  iccdifioo  46231  iccdifprioo  46232  hoiprodp1  47302