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

Theorem difsnid 4126
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 3607 . 2  |-  ( ( A  \  { B } )  u.  { B } )  =  ( { B }  u.  ( A  \  { B } ) )
2 snssi 4124 . . 3  |-  ( B  e.  A  ->  { B }  C_  A )
3 undif 3866 . . 3  |-  ( { B }  C_  A  <->  ( { B }  u.  ( A  \  { B } ) )  =  A )
42, 3sylib 196 . 2  |-  ( B  e.  A  ->  ( { B }  u.  ( A  \  { B }
) )  =  A )
51, 4syl5eq 2507 1  |-  ( B  e.  A  ->  (
( A  \  { B } )  u.  { B } )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758    \ cdif 3432    u. cun 3433    C_ wss 3435   {csn 3984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-sn 3985
This theorem is referenced by:  fnsnsplit  6023  fsnunf2  6025  difsnexi  6493  difsnen  7502  enfixsn  7529  phplem2  7600  pssnn  7641  dif1enOLD  7654  dif1en  7655  frfi  7667  xpfi  7693  dif1card  8287  hashfun  12316  mreexexlem4d  14703  symgextf1  16044  symgextfo  16045  symgfixf1  16061  gsummgp0  16821  islindf4  18391  gsummatr01  18596  tdeglem4  21661  dfconngra1  23708  mgpsumunsn  30906  gsumdifsnd  30909  gsumdifsndf  30912  hdmap14lem4a  35842  hdmap14lem13  35851
  Copyright terms: Public domain W3C validator