Theorem difsnid 4771

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ∖ cdif 3896   ∪ cun 3897   ⊆ wss 3899  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-sn 4585

This theorem is used by:  fnsnsplit  7182  fsnunf2  7184  difsnexi  7760  difsnen  9057  enfixsn  9084  pssnn  9163  dif1ennnALT  9247  frfi  9255  dif1card  10013  hashgt23el  14489  hashfun  14502  fprodfvdvdsd  16424  prmdvdsprmo  17134  mreexexlem4d  17735  symgextf1  19548  symgextfo  19549  symgfixf1  19564  gsumdifsnd  20088  gsummgp0  20458  islindf4  22051  lindsenlbs  22064  scmatf1  22753  gsummatr01  22881  tdeglem4  26285  finsumvtxdg2sstep  30009  dfconngr1  30668  fmptunsnop  33172  satfv1lem  35941  bj-raldifsn  37850  lindsadd  38367  poimirlem25  38394  poimirlem27  38396  hdmap14lem4a  42744  hdmap14lem13  42753  supxrmnf2  46261  infxrpnf2  46291  fsumnncl  46402  hoidmv1lelem2  47420  gsumdifsndf  49096  mgpsumunsn  49291