Theorem difun2 4431

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 4259	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4332	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4138	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4346	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2850	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1537   ∖ cdif 3935   ∪ cun 3936  ∅c0 4293

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294

This theorem is referenced by:  uneqdifeq  4440  difprsn1  4735  orddif  6286  domunsncan  8619  elfiun  8896  hartogslem1  9008  cantnfp1lem3  9145  dju1dif  9600  infdju1  9617  ssxr  10712  dfn2  11913  incexclem  15193  mreexmrid  16916  lbsextlem4  19935  ufprim  22519  volun  24148  i1f1  24293  itgioo  24418  itgsplitioo  24440  plyeq0lem  24802  jensen  25568  difeq  30282  fzdif2  30516  fzodif2  30517  pmtrcnel2  30736  measun  31472  carsgclctunlem1  31577  carsggect  31578  chtvalz  31902  elmrsubrn  32769  mrsubvrs  32771  pibt2  34700  finixpnum  34879  lindsadd  34887  lindsenlbs  34889  poimirlem2  34896  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem11  34905  poimirlem12  34906  poimirlem13  34907  poimirlem14  34908  poimirlem16  34910  poimirlem18  34912  poimirlem19  34913  poimirlem21  34915  poimirlem23  34917  poimirlem27  34921  poimirlem30  34924  asindmre  34979  kelac2  39672  pwfi2f1o  39703  iccdifioo  41798  iccdifprioo  41799  hoiprodp1  42877