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

Theorem difsnid 3761
Description: If we remove a single element from a class then put it back in, we end up with the original class. (Contributed by NM, 2-Oct-2006.)
Assertion
Ref Expression
difsnid  |-  ( B  e.  A  ->  (
( A  \  { B } )  u.  { B } )  =  A )

Proof of Theorem difsnid
StepHypRef Expression
1 uncom 3319 . 2  |-  ( ( A  \  { B } )  u.  { B } )  =  ( { B }  u.  ( A  \  { B } ) )
2 snssi 3759 . . 3  |-  ( B  e.  A  ->  { B }  C_  A )
3 undif 3534 . . 3  |-  ( { B }  C_  A  <->  ( { B }  u.  ( A  \  { B } ) )  =  A )
42, 3sylib 188 . 2  |-  ( B  e.  A  ->  ( { B }  u.  ( A  \  { B }
) )  =  A )
51, 4syl5eq 2327 1  |-  ( B  e.  A  ->  (
( A  \  { B } )  u.  { B } )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684    \ cdif 3149    u. cun 3150    C_ wss 3152   {csn 3640
This theorem is referenced by:  fnsnsplit  5717  fsnunf2  5719  difsnen  6944  phplem2  7041  pssnn  7081  dif1enOLD  7090  dif1en  7091  frfi  7102  xpfi  7128  dif1card  7638  hashfun  11389  mreexexlem4d  13549  tdeglem4  19446  moec  24459  enfixsn  26669  islindf4  26720  hdmap14lem4a  31437  hdmap14lem13  31446
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-sn 3646
  Copyright terms: Public domain W3C validator