Theorem difsnid 4767

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ⊆ wss 3896   ∖ cdif 4044   ∪ cun 4148  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-sn 4585

This theorem is used by:  fnsnsplit  7191  fsnunf2  7193  difsnexi  7777  difsnen  9083  enfixsn  9110  pssnn  9189  dif1ennnALT  9273  frfi  9281  dif1card  10094  hashgt23el  14574  hashfun  14587  fprodfvdvdsd  16511  prmdvdsprmo  17227  mreexexlem4d  17828  symgextf1  19642  symgextfo  19643  symgfixf1  19658  gsumdifsnd  20182  gsummgp0  20554  islindf4  22151  lindsenlbs  22164  scmatf1  22853  gsummatr01  22981  tdeglem4  26385  finsumvtxdg2sstep  30137  dfconngr1  30796  fmptunsnop  33342  satfv1lem  36215  bj-raldifsn  38127  lindsadd  38643  poimirlem25  38670  poimirlem27  38672  hdmap14lem4a  43035  hdmap14lem13  43044  supxrmnf2  46550  infxrpnf2  46580  fsumnncl  46691  hoidmv1lelem2  47709  gsumdifsndf  49385  mgpsumunsn  49580