Theorem difun2 4409

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 4219	. 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵))
2		difid 4304	. . 3 ⊢ (𝐵 ∖ 𝐵) = ∅
3	2	uneq2i 4095	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅)
4		un0 4322	. 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵)
5	1, 3, 4	3eqtri 2766	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1547   ∖ cdif 3880   ∪ cun 3881  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-nul 4262

This theorem is referenced by:  undif5  4412  uneqdifeq  4420  difprsn1  4733  orddif  6408  domunsncan  9005  elfiun  9333  hartogslem1  9447  cantnfp1lem3  9592  dju1dif  10086  infdju1  10103  ssxr  11206  dfn2  12441  incexclem  15792  mreexmrid  17600  lbsextlem4  21154  ufprim  23892  volun  25530  i1f1  25675  itgioo  25801  itgsplitioo  25823  plyeq0lem  26193  jensen  26970  difeq  32606  fzdif2  32882  fzodif2  32883  pmtrcnel2  33171  measun  34395  carsgclctunlem1  34501  carsggect  34502  chtvalz  34813  elmrsubrn  35748  mrsubvrs  35750  pibt2  37779  finixpnum  37972  lindsadd  37980  lindsenlbs  37982  poimirlem2  37989  poimirlem4  37991  poimirlem6  37993  poimirlem7  37994  poimirlem8  37995  poimirlem11  37998  poimirlem12  37999  poimirlem13  38000  poimirlem14  38001  poimirlem16  38003  poimirlem18  38005  poimirlem19  38006  poimirlem21  38008  poimirlem23  38010  poimirlem27  38014  poimirlem30  38017  asindmre  38070  disjresundif  38613  kelac2  43510  pwfi2f1o  43541  iccdifioo  45960  iccdifprioo  45961  hoiprodp1  47031