Theorem difun2 4431

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 4241	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4326	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4115	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4344	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2761	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1541   ∖ cdif 3896   ∪ cun 3897  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-nul 4284

This theorem is referenced by:  undif5  4435  uneqdifeq  4443  difprsn1  4754  orddif  6413  domunsncan  9003  elfiun  9331  hartogslem1  9445  cantnfp1lem3  9587  dju1dif  10081  infdju1  10098  ssxr  11200  dfn2  12412  incexclem  15757  mreexmrid  17564  lbsextlem4  21114  ufprim  23851  volun  25500  i1f1  25645  itgioo  25771  itgsplitioo  25793  plyeq0lem  26169  jensen  26953  difeq  32542  fzdif2  32819  fzodif2  32820  pmtrcnel2  33121  measun  34317  carsgclctunlem1  34423  carsggect  34424  chtvalz  34735  elmrsubrn  35663  mrsubvrs  35665  pibt2  37561  finixpnum  37745  lindsadd  37753  lindsenlbs  37755  poimirlem2  37762  poimirlem4  37764  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  poimirlem11  37771  poimirlem12  37772  poimirlem13  37773  poimirlem14  37774  poimirlem16  37776  poimirlem18  37778  poimirlem19  37779  poimirlem21  37781  poimirlem23  37783  poimirlem27  37787  poimirlem30  37790  asindmre  37843  disjresundif  38381  kelac2  43249  pwfi2f1o  43280  iccdifioo  45703  iccdifprioo  45704  hoiprodp1  46774