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

Theorem difun2 3881
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 3732 . 2  |-  ( ( A  u.  B ) 
\  B )  =  ( ( A  \  B )  u.  ( B  \  B ) )
2 difid 3869 . . 3  |-  ( B 
\  B )  =  (/)
32uneq2i 3623 . 2  |-  ( ( A  \  B )  u.  ( B  \  B ) )  =  ( ( A  \  B )  u.  (/) )
4 un0 3793 . 2  |-  ( ( A  \  B )  u.  (/) )  =  ( A  \  B )
51, 3, 43eqtri 2462 1  |-  ( ( A  u.  B ) 
\  B )  =  ( A  \  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    \ cdif 3439    u. cun 3440   (/)c0 3767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768
This theorem is referenced by:  uneqdifeq  3890  difprsn1  4139  orddif  5535  domunsncan  7678  elfiun  7950  hartogslem1  8057  cantnfp1lem3  8184  cda1dif  8604  infcda1  8621  ssxr  9702  dfn2  10882  incexclem  13872  mreexmrid  15500  lbsextlem4  18319  ufprim  20855  volun  22375  i1f1  22525  itgioo  22650  itgsplitioo  22672  plyeq0lem  23032  jensen  23779  difeq  27987  fzdif2  28205  measun  28872  carsgclctunlem1  28978  carsggect  28979  elmrsubrn  29946  mrsubvrs  29948  finixpnum  31633  poimirlem2  31645  poimirlem4  31647  poimirlem6  31649  poimirlem7  31650  poimirlem8  31651  poimirlem11  31654  poimirlem12  31655  poimirlem13  31656  poimirlem14  31657  poimirlem16  31659  poimirlem18  31661  poimirlem19  31662  poimirlem21  31664  poimirlem23  31666  poimirlem27  31670  poimirlem30  31673  asindmre  31730  kelac2  35628  pwfi2f1o  35659  iccdifioo  37200  iccdifprioo  37201
  Copyright terms: Public domain W3C validator