Theorem difun2 4444

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 4254	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4339	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4128	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4357	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2756	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1540   ∖ cdif 3911   ∪ cun 3912  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-nul 4297

This theorem is referenced by:  undif5  4448  uneqdifeq  4456  difprsn1  4764  orddif  6430  domunsncan  9041  elfiun  9381  hartogslem1  9495  cantnfp1lem3  9633  dju1dif  10126  infdju1  10143  ssxr  11243  dfn2  12455  incexclem  15802  mreexmrid  17604  lbsextlem4  21071  ufprim  23796  volun  25446  i1f1  25591  itgioo  25717  itgsplitioo  25739  plyeq0lem  26115  jensen  26899  difeq  32447  fzdif2  32713  fzodif2  32714  pmtrcnel2  33047  measun  34201  carsgclctunlem1  34308  carsggect  34309  chtvalz  34620  elmrsubrn  35507  mrsubvrs  35509  pibt2  37405  finixpnum  37599  lindsadd  37607  lindsenlbs  37609  poimirlem2  37616  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem16  37630  poimirlem18  37632  poimirlem19  37633  poimirlem21  37635  poimirlem23  37637  poimirlem27  37641  poimirlem30  37644  asindmre  37697  disjresundif  38231  kelac2  43054  pwfi2f1o  43085  iccdifioo  45513  iccdifprioo  45514  hoiprodp1  46586