Theorem difsnid 4777

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

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

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 4592

This theorem is referenced by:  fnsnsplit  7180  fsnunf2  7182  difsnexi  7756  difsnen  9043  enfixsn  9070  pssnn  9149  dif1ennnALT  9233  frfi  9241  dif1card  9990  hashgt23el  14457  hashfun  14470  fprodfvdvdsd  16388  prmdvdsprmo  17098  mreexexlem4d  17699  symgextf1  19487  symgextfo  19488  symgfixf1  19503  gsumdifsnd  20027  gsummgp0  20395  islindf4  21953  scmatf1  22653  gsummatr01  22781  tdeglem4  26182  finsumvtxdg2sstep  29836  dfconngr1  30476  fmptunsnop  32982  satfv1lem  35749  bj-raldifsn  37625  lindsadd  38147  lindsenlbs  38149  poimirlem25  38179  poimirlem27  38181  hdmap14lem4a  42530  hdmap14lem13  42539  supxrmnf2  46034  infxrpnf2  46064  fsumnncl  46175  hoidmv1lelem2  47193  gsumdifsndf  48830  mgpsumunsn  49021