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

Theorem difun2 3439
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 3329 . 2  |-  ( ( A  u.  B ) 
\  B )  =  ( ( A  \  B )  u.  ( B  \  B ) )
2 difid 3428 . . 3  |-  ( B 
\  B )  =  (/)
32uneq2i 3236 . 2  |-  ( ( A  \  B )  u.  ( B  \  B ) )  =  ( ( A  \  B )  u.  (/) )
4 un0 3386 . 2  |-  ( ( A  \  B )  u.  (/) )  =  ( A  \  B )
51, 3, 43eqtri 2277 1  |-  ( ( A  u.  B ) 
\  B )  =  ( A  \  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1619    \ cdif 3075    u. cun 3076   (/)c0 3362
This theorem is referenced by:  uneqdifeq  3448  orddif  4379  domunsncan  6847  elfiun  7067  hartogslem1  7141  cantnfp1lem3  7266  cda1dif  7686  infcda1  7703  ssxr  8772  dfn2  9857  lbsextlem4  15746  ufprim  17436  volun  18734  i1f1  18877  itgioo  19002  itgsplitioo  19024  plyeq0lem  19424  jensen  20115  kelac2  26329  pwfi2f1o  26426
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363
  Copyright terms: Public domain W3C validator