Theorem difun2 4447

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 4252	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4339	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4127	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4358	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2796	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1567   ∖ cdif 3910   ∪ cun 3911  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-nul 4295

This theorem is referenced by:  undif5  4450  uneqdifeq  4458  difprsn1  4772  orddif  6460  domunsncan  9064  elfiun  9389  hartogslem1  9503  cantnfp1lem3  9648  dju1dif  10155  infdju1  10172  ssxr  11278  dfn2  12516  incexclem  15889  mreexmrid  17698  lbsextlem4  21262  ufprim  24034  volun  25672  i1f1  25817  itgioo  25943  itgsplitioo  25965  plyeq0lem  26335  jensen  27118  difeq  32804  fzdif2  33075  fzodif2  33076  pmtrcnel2  33350  measun  34545  carsgclctunlem1  34651  carsggect  34652  chtvalz  34960  elmrsubrn  35910  mrsubvrs  35912  pibt2  37950  finixpnum  38143  lindsadd  38151  lindsenlbs  38153  poimirlem2  38160  poimirlem4  38162  poimirlem6  38164  poimirlem7  38165  poimirlem8  38166  poimirlem11  38169  poimirlem12  38170  poimirlem13  38171  poimirlem14  38172  poimirlem16  38174  poimirlem18  38176  poimirlem19  38177  poimirlem21  38179  poimirlem23  38181  poimirlem27  38185  poimirlem30  38188  asindmre  38241  disjresundif  38784  kelac2  43683  pwfi2f1o  43714  iccdifioo  46122  iccdifprioo  46123  hoiprodp1  47193