Theorem difun2 4411

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 4211	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4301	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4090	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4321	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2770	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1539   ∖ cdif 3880   ∪ cun 3881  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-nul 4254

This theorem is referenced by:  uneqdifeq  4420  difprsn1  4730  orddif  6344  domunsncan  8812  elfiun  9119  hartogslem1  9231  cantnfp1lem3  9368  dju1dif  9859  infdju1  9876  ssxr  10975  dfn2  12176  incexclem  15476  mreexmrid  17269  lbsextlem4  20338  ufprim  22968  volun  24614  i1f1  24759  itgioo  24885  itgsplitioo  24907  plyeq0lem  25276  jensen  26043  difeq  30766  undif5  30768  fzdif2  31014  fzodif2  31015  pmtrcnel2  31261  measun  32079  carsgclctunlem1  32184  carsggect  32185  chtvalz  32509  elmrsubrn  33382  mrsubvrs  33384  pibt2  35515  finixpnum  35689  lindsadd  35697  lindsenlbs  35699  poimirlem2  35706  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem16  35720  poimirlem18  35722  poimirlem19  35723  poimirlem21  35725  poimirlem23  35727  poimirlem27  35731  poimirlem30  35734  asindmre  35787  kelac2  40806  pwfi2f1o  40837  iccdifioo  42943  iccdifprioo  42944  hoiprodp1  44016