Theorem difsnid 4780

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   ∖ cdif 3910   ∪ cun 3911   ⊆ wss 3913  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-sn 4595

This theorem is referenced by:  fnsnsplit  7183  fsnunf2  7185  difsnexi  7760  difsnen  9047  enfixsn  9074  pssnn  9153  dif1ennnALT  9237  frfi  9245  dif1card  9994  hashgt23el  14461  hashfun  14474  fprodfvdvdsd  16392  prmdvdsprmo  17102  mreexexlem4d  17703  symgextf1  19491  symgextfo  19492  symgfixf1  19507  gsumdifsnd  20031  gsummgp0  20399  islindf4  21957  scmatf1  22657  gsummatr01  22785  tdeglem4  26186  finsumvtxdg2sstep  29840  dfconngr1  30480  fmptunsnop  32986  satfv1lem  35753  bj-raldifsn  37630  lindsadd  38152  lindsenlbs  38154  poimirlem25  38184  poimirlem27  38186  hdmap14lem4a  42535  hdmap14lem13  42544  supxrmnf2  46039  infxrpnf2  46069  fsumnncl  46180  hoidmv1lelem2  47198  gsumdifsndf  48835  mgpsumunsn  49026