MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difun2 Structured version   Unicode version

Theorem difun2 3877
Description: Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
Assertion
Ref Expression
difun2  |-  ( ( A  u.  B ) 
\  B )  =  ( A  \  B
)

Proof of Theorem difun2
StepHypRef Expression
1 difundir 3726 . 2  |-  ( ( A  u.  B ) 
\  B )  =  ( ( A  \  B )  u.  ( B  \  B ) )
2 difid 3865 . . 3  |-  ( B 
\  B )  =  (/)
32uneq2i 3617 . 2  |-  ( ( A  \  B )  u.  ( B  \  B ) )  =  ( ( A  \  B )  u.  (/) )
4 un0 3789 . 2  |-  ( ( A  \  B )  u.  (/) )  =  ( A  \  B )
51, 3, 43eqtri 2455 1  |-  ( ( A  u.  B ) 
\  B )  =  ( A  \  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    \ cdif 3433    u. cun 3434   (/)c0 3761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762
This theorem is referenced by:  uneqdifeq  3886  difprsn1  4136  orddif  5535  domunsncan  7681  elfiun  7953  hartogslem1  8066  cantnfp1lem3  8193  cda1dif  8613  infcda1  8630  ssxr  9710  dfn2  10889  incexclem  13893  mreexmrid  15548  lbsextlem4  18383  ufprim  20922  volun  22496  i1f1  22646  itgioo  22771  itgsplitioo  22793  plyeq0lem  23162  jensen  23912  difeq  28150  fzdif2  28375  measun  29041  carsgclctunlem1  29157  carsggect  29158  elmrsubrn  30166  mrsubvrs  30168  finixpnum  31894  poimirlem2  31906  poimirlem4  31908  poimirlem6  31910  poimirlem7  31911  poimirlem8  31912  poimirlem11  31915  poimirlem12  31916  poimirlem13  31917  poimirlem14  31918  poimirlem16  31920  poimirlem18  31922  poimirlem19  31923  poimirlem21  31925  poimirlem23  31927  poimirlem27  31931  poimirlem30  31934  asindmre  31991  kelac2  35893  pwfi2f1o  35924  iccdifioo  37565  iccdifprioo  37566  hoiprodp1  38314
  Copyright terms: Public domain W3C validator