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

Theorem difsnid 4809
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 (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Proof of Theorem difsnid
StepHypRef Expression
1 snssi 4807 . 2 (𝐵𝐴 → {𝐵} ⊆ 𝐴)
2 undifr 4482 . 2 ({𝐵} ⊆ 𝐴 ↔ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
31, 2sylib 218 1 (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wcel 2107  cdif 3947  cun 3948  wss 3950  {csn 4625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-sn 4626
This theorem is referenced by:  fnsnsplit  7205  fsnunf2  7207  difsnexi  7782  difsnen  9094  enfixsn  9122  pssnn  9209  phplem2OLD  9256  dif1ennnALT  9312  frfi  9322  xpfiOLD  9360  dif1card  10051  hashgt23el  14464  hashfun  14477  fprodfvdvdsd  16372  prmdvdsprmo  17081  mreexexlem4d  17691  symgextf1  19440  symgextfo  19441  symgfixf1  19456  gsumdifsnd  19980  gsummgp0  20316  islindf4  21859  scmatf1  22538  gsummatr01  22666  tdeglem4  26100  finsumvtxdg2sstep  29568  dfconngr1  30208  fmptunsnop  32710  satfv1lem  35368  bj-raldifsn  37102  lindsadd  37621  lindsenlbs  37623  poimirlem25  37653  poimirlem27  37655  hdmap14lem4a  41874  hdmap14lem13  41883  supxrmnf2  45449  infxrpnf2  45479  fsumnncl  45592  hoidmv1lelem2  46612  gsumdifsndf  48102  mgpsumunsn  48282
  Copyright terms: Public domain W3C validator