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 2788	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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-nul 4280

This theorem is used by:  undif5  4440  uneqdifeq  4448  difprsn1  4763  orddif  6461  domunsncan  9096  elfiun  9422  hartogslem1  9536  cantnfp1lem3  9681  dju1dif  10251  infdju1  10268  ssxr  11379  dfn2  12619  incexclem  16005  mreexmrid  17817  lbsextlem4  21439  lindsenlbs  22157  ufprim  24228  volun  25866  i1f1  26011  itgioo  26136  itgsplitioo  26158  plyeq0lem  26529  jensen  27316  difeq  33114  fzdif2  33382  fzodif2  33383  pmtrcnel2  33651  measun  34844  carsgclctunlem1  34949  carsggect  34950  chtvalz  35258  elmrsubrn  36285  mrsubvrs  36287  pibt2  38340  finixpnum  38528  lindsadd  38536  poimirlem2  38540  poimirlem4  38542  poimirlem6  38544  poimirlem7  38545  poimirlem8  38546  poimirlem11  38549  poimirlem12  38550  poimirlem13  38551  poimirlem14  38552  poimirlem16  38554  poimirlem18  38556  poimirlem19  38557  poimirlem21  38559  poimirlem23  38561  poimirlem27  38565  poimirlem30  38568  asindmre  38621  disjresundif  39178  kelac2  44066  pwfi2f1o  44097  iccdifioo  46526  iccdifprioo  46527  hoiprodp1  47597