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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-sn 4585

This theorem is used by:  fnsnsplit  7187  fsnunf2  7189  difsnexi  7773  difsnen  9071  enfixsn  9098  pssnn  9177  dif1ennnALT  9261  frfi  9269  dif1card  10082  hashgt23el  14562  hashfun  14575  fprodfvdvdsd  16497  prmdvdsprmo  17213  mreexexlem4d  17814  symgextf1  19628  symgextfo  19629  symgfixf1  19644  gsumdifsnd  20168  gsummgp0  20540  islindf4  22137  lindsenlbs  22150  scmatf1  22839  gsummatr01  22967  tdeglem4  26371  finsumvtxdg2sstep  30123  dfconngr1  30782  fmptunsnop  33286  satfv1lem  36106  bj-raldifsn  38001  lindsadd  38516  poimirlem25  38543  poimirlem27  38545  hdmap14lem4a  42908  hdmap14lem13  42917  supxrmnf2  46412  infxrpnf2  46442  fsumnncl  46553  hoidmv1lelem2  47571  gsumdifsndf  49247  mgpsumunsn  49442