Theorem difun2 4433

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 4243	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4328	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4117	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4346	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2763	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1541   ∖ cdif 3898   ∪ cun 3899  ∅c0 4285

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-nul 4286

This theorem is referenced by:  undif5  4437  uneqdifeq  4445  difprsn1  4756  orddif  6415  domunsncan  9005  elfiun  9333  hartogslem1  9447  cantnfp1lem3  9589  dju1dif  10083  infdju1  10100  ssxr  11202  dfn2  12414  incexclem  15759  mreexmrid  17566  lbsextlem4  21116  ufprim  23853  volun  25502  i1f1  25647  itgioo  25773  itgsplitioo  25795  plyeq0lem  26171  jensen  26955  difeq  32593  fzdif2  32870  fzodif2  32871  pmtrcnel2  33172  measun  34368  carsgclctunlem1  34474  carsggect  34475  chtvalz  34786  elmrsubrn  35714  mrsubvrs  35716  pibt2  37622  finixpnum  37806  lindsadd  37814  lindsenlbs  37816  poimirlem2  37823  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem11  37832  poimirlem12  37833  poimirlem13  37834  poimirlem14  37835  poimirlem16  37837  poimirlem18  37839  poimirlem19  37840  poimirlem21  37842  poimirlem23  37844  poimirlem27  37848  poimirlem30  37851  asindmre  37904  disjresundif  38442  kelac2  43307  pwfi2f1o  43338  iccdifioo  45761  iccdifprioo  45762  hoiprodp1  46832