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

Theorem difun2 3906
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 3751 . 2  |-  ( ( A  u.  B ) 
\  B )  =  ( ( A  \  B )  u.  ( B  \  B ) )
2 difid 3895 . . 3  |-  ( B 
\  B )  =  (/)
32uneq2i 3655 . 2  |-  ( ( A  \  B )  u.  ( B  \  B ) )  =  ( ( A  \  B )  u.  (/) )
4 un0 3810 . 2  |-  ( ( A  \  B )  u.  (/) )  =  ( A  \  B )
51, 3, 43eqtri 2500 1  |-  ( ( A  u.  B ) 
\  B )  =  ( A  \  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    \ cdif 3473    u. cun 3474   (/)c0 3785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786
This theorem is referenced by:  uneqdifeq  3915  difprsn1  4163  orddif  4971  domunsncan  7617  elfiun  7889  hartogslem1  7966  cantnfp1lem3  8098  cantnfp1lem3OLD  8124  cda1dif  8555  infcda1  8572  ssxr  9653  dfn2  10807  incexclem  13610  mreexmrid  14897  lbsextlem4  17602  ufprim  20161  volun  21706  i1f1  21848  itgioo  21973  itgsplitioo  21995  plyeq0lem  22358  jensen  23062  difeq  27106  measun  27838  finixpnum  29631  asindmre  29695  kelac2  30631  pwfi2f1o  30664  iccdifioo  31135  iccdifprioo  31136
  Copyright terms: Public domain W3C validator