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

Theorem difsnid 4007
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 3488 . 2  |-  ( ( A  \  { B } )  u.  { B } )  =  ( { B }  u.  ( A  \  { B } ) )
2 snssi 4005 . . 3  |-  ( B  e.  A  ->  { B }  C_  A )
3 undif 3747 . . 3  |-  ( { B }  C_  A  <->  ( { B }  u.  ( A  \  { B } ) )  =  A )
42, 3sylib 196 . 2  |-  ( B  e.  A  ->  ( { B }  u.  ( A  \  { B }
) )  =  A )
51, 4syl5eq 2477 1  |-  ( B  e.  A  ->  (
( A  \  { B } )  u.  { B } )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755    \ cdif 3313    u. cun 3314    C_ wss 3316   {csn 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-sn 3866
This theorem is referenced by:  fnsnsplit  5902  fsnunf2  5904  difsnexi  6373  difsnen  7381  enfixsn  7408  phplem2  7479  pssnn  7519  dif1enOLD  7532  dif1en  7533  frfi  7545  xpfi  7571  dif1card  8165  hashfun  12183  mreexexlem4d  14568  symgextf1  15906  symgextfo  15907  symgfixf1  15923  gsummgp0  16634  islindf4  18109  gsummatr01  18307  tdeglem4  21414  dfconngra1  23380  mgpsumunsn  30594  gsumdifsnd  30597  hdmap14lem4a  35113  hdmap14lem13  35122
  Copyright terms: Public domain W3C validator