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

Theorem difsnid 4310
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 3735 . 2 ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = ({𝐵} ∪ (𝐴 ∖ {𝐵}))
2 snssi 4308 . . 3 (𝐵𝐴 → {𝐵} ⊆ 𝐴)
3 undif 4021 . . 3 ({𝐵} ⊆ 𝐴 ↔ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
42, 3sylib 208 . 2 (𝐵𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
51, 4syl5eq 2667 1 (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  cdif 3552  cun 3553  wss 3555  {csn 4148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-sn 4149
This theorem is referenced by:  fnsnsplit  6404  fsnunf2  6406  difsnexi  6919  difsnen  7986  enfixsn  8013  phplem2  8084  pssnn  8122  dif1en  8137  frfi  8149  xpfi  8175  dif1card  8777  hashfun  13164  fprodfvdvdsd  14982  prmdvdsprmo  15670  mreexexlem4d  16228  symgextf1  17762  symgextfo  17763  symgfixf1  17778  gsumdifsnd  18281  gsummgp0  18529  islindf4  20096  scmatf1  20256  gsummatr01  20384  tdeglem4  23724  dfconngr1  26914  lindsenlbs  33036  poimirlem25  33066  poimirlem27  33068  hdmap14lem4a  36643  hdmap14lem13  36652  fsumnncl  39207  hoidmv1lelem2  40113  mgpsumunsn  41428  gsumdifsndf  41432
  Copyright terms: Public domain W3C validator