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

Theorem difsnid 4162
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 3634 . 2  |-  ( ( A  \  { B } )  u.  { B } )  =  ( { B }  u.  ( A  \  { B } ) )
2 snssi 4160 . . 3  |-  ( B  e.  A  ->  { B }  C_  A )
3 undif 3896 . . 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 1398    e. wcel 1823    \ cdif 3458    u. cun 3459    C_ wss 3461   {csn 4016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-sn 4017
This theorem is referenced by:  fnsnsplit  6084  fsnunf2  6086  difsnexi  6581  difsnen  7592  enfixsn  7619  phplem2  7690  pssnn  7731  dif1en  7745  frfi  7757  xpfi  7783  dif1card  8379  hashfun  12482  mreexexlem4d  15139  symgextf1  16648  symgextfo  16649  symgfixf1  16664  gsumdifsnd  17186  gsummgp0  17454  islindf4  19043  scmatf1  19203  gsummatr01  19331  tdeglem4  22627  dfconngra1  24876  fsumnncl  31814  mgpsumunsn  33224  gsumdifsndf  33228  hdmap14lem4a  38017  hdmap14lem13  38026
  Copyright terms: Public domain W3C validator