Theorem difun2 4437

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 4237	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4325	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4112	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4344	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2787	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3896   ∪ cun 3897  ∅c0 4279

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-nul 4280

This theorem is used by:  undif5  4440  uneqdifeq  4448  difprsn1  4763  orddif  6456  domunsncan  9076  elfiun  9401  hartogslem1  9515  cantnfp1lem3  9660  dju1dif  10176  infdju1  10193  ssxr  11304  dfn2  12542  incexclem  15926  mreexmrid  17732  lbsextlem4  21349  lindsenlbs  22065  ufprim  24136  volun  25774  i1f1  25919  itgioo  26044  itgsplitioo  26066  plyeq0lem  26437  jensen  27226  difeq  32994  fzdif2  33262  fzodif2  33263  pmtrcnel2  33531  measun  34723  carsgclctunlem1  34829  carsggect  34830  chtvalz  35138  elmrsubrn  36100  mrsubvrs  36102  pibt2  38172  finixpnum  38360  lindsadd  38368  poimirlem2  38372  poimirlem4  38374  poimirlem6  38376  poimirlem7  38377  poimirlem8  38378  poimirlem11  38381  poimirlem12  38382  poimirlem13  38383  poimirlem14  38384  poimirlem16  38386  poimirlem18  38388  poimirlem19  38389  poimirlem21  38391  poimirlem23  38393  poimirlem27  38397  poimirlem30  38400  asindmre  38453  disjresundif  38995  kelac2  43907  pwfi2f1o  43938  iccdifioo  46346  iccdifprioo  46347  hoiprodp1  47417