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  32734  fzodif2  32735  pmtrcnel2  33033  measun  34184  carsgclctunlem1  34291  carsggect  34292  chtvalz  34603  elmrsubrn  35503  mrsubvrs  35505  pibt2  37401  finixpnum  37595  lindsadd  37603  lindsenlbs  37605  poimirlem2  37612  poimirlem4  37614  poimirlem6  37616  poimirlem7  37617  poimirlem8  37618  poimirlem11  37621  poimirlem12  37622  poimirlem13  37623  poimirlem14  37624  poimirlem16  37626  poimirlem18  37628  poimirlem19  37629  poimirlem21  37631  poimirlem23  37633  poimirlem27  37637  poimirlem30  37640  asindmre  37693  disjresundif  38227  kelac2  43048  pwfi2f1o  43079  iccdifioo  45506  iccdifprioo  45507  hoiprodp1  46579