Theorem difun2 4487

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 4297	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4382	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4175	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4400	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2767	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1537   ∖ cdif 3960   ∪ cun 3961  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-nul 4340

This theorem is referenced by:  undif5  4491  uneqdifeq  4499  difprsn1  4805  orddif  6482  domunsncan  9111  elfiun  9468  hartogslem1  9580  cantnfp1lem3  9718  dju1dif  10211  infdju1  10228  ssxr  11328  dfn2  12537  incexclem  15869  mreexmrid  17688  lbsextlem4  21181  ufprim  23933  volun  25594  i1f1  25739  itgioo  25866  itgsplitioo  25888  plyeq0lem  26264  jensen  27047  difeq  32546  fzdif2  32799  fzodif2  32800  pmtrcnel2  33093  measun  34192  carsgclctunlem1  34299  carsggect  34300  chtvalz  34623  elmrsubrn  35505  mrsubvrs  35507  pibt2  37400  finixpnum  37592  lindsadd  37600  lindsenlbs  37602  poimirlem2  37609  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem11  37618  poimirlem12  37619  poimirlem13  37620  poimirlem14  37621  poimirlem16  37623  poimirlem18  37625  poimirlem19  37626  poimirlem21  37628  poimirlem23  37630  poimirlem27  37634  poimirlem30  37637  asindmre  37690  disjresundif  38224  kelac2  43054  pwfi2f1o  43085  iccdifioo  45468  iccdifprioo  45469  hoiprodp1  46544