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

Theorem difun2 3534
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 3423 . 2  |-  ( ( A  u.  B ) 
\  B )  =  ( ( A  \  B )  u.  ( B  \  B ) )
2 difid 3523 . . 3  |-  ( B 
\  B )  =  (/)
32uneq2i 3327 . 2  |-  ( ( A  \  B )  u.  ( B  \  B ) )  =  ( ( A  \  B )  u.  (/) )
4 un0 3480 . 2  |-  ( ( A  \  B )  u.  (/) )  =  ( A  \  B )
51, 3, 43eqtri 2308 1  |-  ( ( A  u.  B ) 
\  B )  =  ( A  \  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1628    \ cdif 3150    u. cun 3151   (/)c0 3456
This theorem is referenced by:  uneqdifeq  3543  orddif  4485  domunsncan  6957  elfiun  7178  hartogslem1  7252  cantnfp1lem3  7377  cda1dif  7797  infcda1  7814  ssxr  8887  dfn2  9973  incexclem  12289  mreexmrid  13539  lbsextlem4  15908  ufprim  17598  volun  18896  i1f1  19039  itgioo  19164  itgsplitioo  19186  plyeq0lem  19586  jensen  20277  kelac2  26562  pwfi2f1o  26659
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457
  Copyright terms: Public domain W3C validator