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

Theorem difun2 3699
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 3586 . 2  |-  ( ( A  u.  B ) 
\  B )  =  ( ( A  \  B )  u.  ( B  \  B ) )
2 difid 3688 . . 3  |-  ( B 
\  B )  =  (/)
32uneq2i 3490 . 2  |-  ( ( A  \  B )  u.  ( B  \  B ) )  =  ( ( A  \  B )  u.  (/) )
4 un0 3644 . 2  |-  ( ( A  \  B )  u.  (/) )  =  ( A  \  B )
51, 3, 43eqtri 2459 1  |-  ( ( A  u.  B ) 
\  B )  =  ( A  \  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1652    \ cdif 3309    u. cun 3310   (/)c0 3620
This theorem is referenced by:  uneqdifeq  3708  difprsn1  3927  orddif  4666  domunsncan  7199  elfiun  7426  hartogslem1  7500  cantnfp1lem3  7625  cda1dif  8045  infcda1  8062  ssxr  9134  dfn2  10223  incexclem  12604  mreexmrid  13856  lbsextlem4  16221  ufprim  17929  volun  19427  i1f1  19570  itgioo  19695  itgsplitioo  19717  plyeq0lem  20117  jensen  20815  difeq  23986  measun  24553  kelac2  27078  pwfi2f1o  27175
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621
  Copyright terms: Public domain W3C validator