Theorem difsnid 4765

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 4741	. 2 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴)
2		undifr 4434	. 2 ⊢ ({𝐵} ⊆ 𝐴 ↔ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
3	1, 2	sylib 220	1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141   ∖ cdif 3899   ∪ cun 3900   ⊆ wss 3902  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-sn 4580

This theorem is referenced by:  fnsnsplit  7163  fsnunf2  7165  difsnexi  7739  difsnen  9025  enfixsn  9052  pssnn  9131  dif1ennnALT  9215  frfi  9223  dif1card  9960  hashgt23el  14431  hashfun  14444  fprodfvdvdsd  16359  prmdvdsprmo  17069  mreexexlem4d  17670  symgextf1  19452  symgextfo  19453  symgfixf1  19468  gsumdifsnd  19992  gsummgp0  20353  islindf4  21878  scmatf1  22579  gsummatr01  22707  tdeglem4  26108  finsumvtxdg2sstep  29707  dfconngr1  30347  fmptunsnop  32863  satfv1lem  35673  bj-raldifsn  37551  lindsadd  38073  lindsenlbs  38075  poimirlem25  38105  poimirlem27  38107  hdmap14lem4a  42456  hdmap14lem13  42465  supxrmnf2  45968  infxrpnf2  45998  fsumnncl  46109  hoidmv1lelem2  47127  gsumdifsndf  48764  mgpsumunsn  48944