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

Theorem difsnid 4373
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 uncom 3790 . 2 ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = ({𝐵} ∪ (𝐴 ∖ {𝐵}))
2 snssi 4371 . . 3 (𝐵𝐴 → {𝐵} ⊆ 𝐴)
3 undif 4082 . . 3 ({𝐵} ⊆ 𝐴 ↔ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
42, 3sylib 208 . 2 (𝐵𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
51, 4syl5eq 2697 1 (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  cdif 3604  cun 3605  wss 3607  {csn 4210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-sn 4211
This theorem is referenced by:  fnsnsplit  6491  fsnunf2  6493  difsnexi  7012  difsnen  8083  enfixsn  8110  phplem2  8181  pssnn  8219  dif1en  8234  frfi  8246  xpfi  8272  dif1card  8871  hashfun  13262  fprodfvdvdsd  15105  prmdvdsprmo  15793  mreexexlem4d  16354  symgextf1  17887  symgextfo  17888  symgfixf1  17903  gsumdifsnd  18406  gsummgp0  18654  islindf4  20225  scmatf1  20385  gsummatr01  20513  tdeglem4  23865  finsumvtxdg2sstep  26501  dfconngr1  27166  bj-raldifsn  33179  lindsenlbs  33534  poimirlem25  33564  poimirlem27  33566  hdmap14lem4a  37480  hdmap14lem13  37489  supxrmnf2  39973  infxrpnf2  40006  fsumnncl  40121  hoidmv1lelem2  41127  mgpsumunsn  42465  gsumdifsndf  42469
  Copyright terms: Public domain W3C validator