Theorem difun2 4432

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 4242	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4327	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4116	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4345	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2756	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1540   ∖ cdif 3900   ∪ cun 3901  ∅c0 4284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-nul 4285

This theorem is referenced by:  undif5  4436  uneqdifeq  4444  difprsn1  4751  orddif  6405  domunsncan  8994  elfiun  9320  hartogslem1  9434  cantnfp1lem3  9576  dju1dif  10067  infdju1  10084  ssxr  11185  dfn2  12397  incexclem  15743  mreexmrid  17549  lbsextlem4  21068  ufprim  23794  volun  25444  i1f1  25589  itgioo  25715  itgsplitioo  25737  plyeq0lem  26113  jensen  26897  difeq  32462  fzdif2  32733  fzodif2  32734  pmtrcnel2  33032  measun  34178  carsgclctunlem1  34285  carsggect  34286  chtvalz  34597  elmrsubrn  35497  mrsubvrs  35499  pibt2  37395  finixpnum  37589  lindsadd  37597  lindsenlbs  37599  poimirlem2  37606  poimirlem4  37608  poimirlem6  37610  poimirlem7  37611  poimirlem8  37612  poimirlem11  37615  poimirlem12  37616  poimirlem13  37617  poimirlem14  37618  poimirlem16  37620  poimirlem18  37622  poimirlem19  37623  poimirlem21  37625  poimirlem23  37627  poimirlem27  37631  poimirlem30  37634  asindmre  37687  disjresundif  38221  kelac2  43042  pwfi2f1o  43073  iccdifioo  45500  iccdifprioo  45501  hoiprodp1  46573