Theorem difun2 4440

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 4239	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4328	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4167	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4347	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2790	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 4048   ∪ cun 4152  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282

This theorem is used by:  undif5  4443  uneqdifeq  4451  difprsn1  4765  orddif  6487  domunsncan  9134  elfiun  9459  hartogslem1  9573  cantnfp1lem3  9718  dju1dif  10290  infdju1  10307  ssxr  11418  dfn2  12659  incexclem  16049  mreexmrid  17867  lbsextlem4  21490  lindsenlbs  22212  ufprim  24283  volun  25921  i1f1  26066  itgioo  26191  itgsplitioo  26213  plyeq0lem  26584  jensen  27373  difeq  33213  fzdif2  33478  fzodif2  33479  pmtrcnel2  33750  measun  34955  carsgclctunlem1  35060  carsggect  35061  chtvalz  35369  elmrsubrn  36493  mrsubvrs  36495  pibt2  38608  finixpnum  38796  lindsadd  38804  poimirlem2  38808  poimirlem4  38810  poimirlem6  38812  poimirlem7  38813  poimirlem8  38814  poimirlem11  38817  poimirlem12  38818  poimirlem13  38819  poimirlem14  38820  poimirlem16  38822  poimirlem18  38824  poimirlem19  38825  poimirlem21  38827  poimirlem23  38829  poimirlem27  38833  poimirlem30  38836  asindmre  38889  disjresundif  39444  kelac2  44333  pwfi2f1o  44364  iccdifioo  46800  iccdifprioo  46801  hoiprodp1  47871