Theorem difsnid 4776

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ∖ cdif 3902   ∪ cun 3903   ⊆ wss 3905  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-sn 4590

This theorem is referenced by:  fnsnsplit  7182  fsnunf2  7184  difsnexi  7756  difsnen  9043  enfixsn  9070  pssnn  9149  dif1ennnALT  9233  frfi  9241  dif1card  9990  hashgt23el  14457  hashfun  14470  fprodfvdvdsd  16387  prmdvdsprmo  17097  mreexexlem4d  17698  symgextf1  19486  symgextfo  19487  symgfixf1  19502  gsumdifsnd  20026  gsummgp0  20395  islindf4  21988  scmatf1  22688  gsummatr01  22816  tdeglem4  26217  finsumvtxdg2sstep  29899  dfconngr1  30539  fmptunsnop  33045  satfv1lem  35854  bj-raldifsn  37742  lindsadd  38264  lindsenlbs  38266  poimirlem25  38296  poimirlem27  38298  hdmap14lem4a  42645  hdmap14lem13  42654  supxrmnf2  46147  infxrpnf2  46177  fsumnncl  46288  hoidmv1lelem2  47306  gsumdifsndf  48946  mgpsumunsn  49141