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

Theorem difun2 3508
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 3397 . 2  |-  ( ( A  u.  B ) 
\  B )  =  ( ( A  \  B )  u.  ( B  \  B ) )
2 difid 3497 . . 3  |-  ( B 
\  B )  =  (/)
32uneq2i 3301 . 2  |-  ( ( A  \  B )  u.  ( B  \  B ) )  =  ( ( A  \  B )  u.  (/) )
4 un0 3454 . 2  |-  ( ( A  \  B )  u.  (/) )  =  ( A  \  B )
51, 3, 43eqtri 2282 1  |-  ( ( A  u.  B ) 
\  B )  =  ( A  \  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1619    \ cdif 3124    u. cun 3125   (/)c0 3430
This theorem is referenced by:  uneqdifeq  3517  orddif  4458  domunsncan  6930  elfiun  7151  hartogslem1  7225  cantnfp1lem3  7350  cda1dif  7770  infcda1  7787  ssxr  8860  dfn2  9945  mreexmrid  13507  lbsextlem4  15876  ufprim  17566  volun  18864  i1f1  19007  itgioo  19132  itgsplitioo  19154  plyeq0lem  19554  jensen  20245  kelac2  26530  pwfi2f1o  26627
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 1927  ax-ext 2239
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431
  Copyright terms: Public domain W3C validator