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 4244	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4332	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4119	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4351	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2792	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3903   ∪ cun 3904  ∅c0 4286

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-nul 4287

This theorem is used by:  undif5  4447  uneqdifeq  4455  difprsn1  4770  orddif  6463  domunsncan  9072  elfiun  9397  hartogslem1  9511  cantnfp1lem3  9656  dju1dif  10172  infdju1  10189  ssxr  11294  dfn2  12532  incexclem  15913  mreexmrid  17721  lbsextlem4  21335  ufprim  24117  volun  25755  i1f1  25900  itgioo  26026  itgsplitioo  26048  plyeq0lem  26418  jensen  27204  difeq  32935  fzdif2  33205  fzodif2  33206  pmtrcnel2  33474  measun  34666  carsgclctunlem1  34772  carsggect  34773  chtvalz  35081  elmrsubrn  36049  mrsubvrs  36051  pibt2  38120  finixpnum  38313  lindsadd  38321  lindsenlbs  38323  poimirlem2  38330  poimirlem4  38332  poimirlem6  38334  poimirlem7  38335  poimirlem8  38336  poimirlem11  38339  poimirlem12  38340  poimirlem13  38341  poimirlem14  38342  poimirlem16  38344  poimirlem18  38346  poimirlem19  38347  poimirlem21  38349  poimirlem23  38351  poimirlem27  38355  poimirlem30  38358  asindmre  38411  disjresundif  38953  kelac2  43850  pwfi2f1o  43881  iccdifioo  46289  iccdifprioo  46290  hoiprodp1  47360