Theorem difun2 4421

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 4231	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4316	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4105	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4334	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2763	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1542   ∖ cdif 3886   ∪ cun 3887  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-nul 4274

This theorem is referenced by:  undif5  4424  uneqdifeq  4432  difprsn1  4745  orddif  6421  domunsncan  9015  elfiun  9343  hartogslem1  9457  cantnfp1lem3  9601  dju1dif  10095  infdju1  10112  ssxr  11215  dfn2  12450  incexclem  15801  mreexmrid  17609  lbsextlem4  21159  ufprim  23874  volun  25512  i1f1  25657  itgioo  25783  itgsplitioo  25805  plyeq0lem  26175  jensen  26952  difeq  32588  fzdif2  32863  fzodif2  32864  pmtrcnel2  33151  measun  34355  carsgclctunlem1  34461  carsggect  34462  chtvalz  34773  elmrsubrn  35702  mrsubvrs  35704  pibt2  37733  finixpnum  37926  lindsadd  37934  lindsenlbs  37936  poimirlem2  37943  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem16  37957  poimirlem18  37959  poimirlem19  37960  poimirlem21  37962  poimirlem23  37964  poimirlem27  37968  poimirlem30  37971  asindmre  38024  disjresundif  38567  kelac2  43493  pwfi2f1o  43524  iccdifioo  45945  iccdifprioo  45946  hoiprodp1  47016