Theorem difsnid 4754

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

Step	Hyp	Ref	Expression
1		snssi 4752	. 2 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴)
2		undifr 4424	. 2 ⊢ ({𝐵} ⊆ 𝐴 ↔ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
3	1, 2	sylib 218	1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∖ cdif 3887   ∪ cun 3888   ⊆ wss 3890  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-sn 4569

This theorem is referenced by:  fnsnsplit  7132  fsnunf2  7134  difsnexi  7708  difsnen  8990  enfixsn  9017  pssnn  9096  dif1ennnALT  9180  frfi  9188  dif1card  9923  hashgt23el  14377  hashfun  14390  fprodfvdvdsd  16294  prmdvdsprmo  17004  mreexexlem4d  17604  symgextf1  19387  symgextfo  19388  symgfixf1  19403  gsumdifsnd  19927  gsummgp0  20288  islindf4  21828  scmatf1  22506  gsummatr01  22634  tdeglem4  26035  finsumvtxdg2sstep  29633  dfconngr1  30273  fmptunsnop  32788  satfv1lem  35560  bj-raldifsn  37428  lindsadd  37948  lindsenlbs  37950  poimirlem25  37980  poimirlem27  37982  hdmap14lem4a  42331  hdmap14lem13  42340  supxrmnf2  45879  infxrpnf2  45909  fsumnncl  46020  hoidmv1lelem2  47038  gsumdifsndf  48669  mgpsumunsn  48849