Theorem difun2 4440

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 4240	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4328	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4115	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4347	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2789	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3899   ∪ cun 3900  ∅c0 4282

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-nul 4283

This theorem is used by:  undif5  4443  uneqdifeq  4451  difprsn1  4766  orddif  6460  domunsncan  9079  elfiun  9404  hartogslem1  9518  cantnfp1lem3  9663  dju1dif  10179  infdju1  10196  ssxr  11307  dfn2  12545  incexclem  15929  mreexmrid  17737  lbsextlem4  21354  lindsenlbs  22070  ufprim  24141  volun  25779  i1f1  25924  itgioo  26050  itgsplitioo  26072  plyeq0lem  26443  jensen  27233  difeq  33001  fzdif2  33269  fzodif2  33270  pmtrcnel2  33538  measun  34730  carsgclctunlem1  34836  carsggect  34837  chtvalz  35145  elmrsubrn  36107  mrsubvrs  36109  pibt2  38179  finixpnum  38367  lindsadd  38375  poimirlem2  38379  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem11  38388  poimirlem12  38389  poimirlem13  38390  poimirlem14  38391  poimirlem16  38393  poimirlem18  38395  poimirlem19  38396  poimirlem21  38398  poimirlem23  38400  poimirlem27  38404  poimirlem30  38407  asindmre  38460  disjresundif  39002  kelac2  43914  pwfi2f1o  43945  iccdifioo  46353  iccdifprioo  46354  hoiprodp1  47424