Theorem difsnid 4773

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ⊆ wss 3900   ∖ cdif 4048   ∪ cun 4152  {csn 4588

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-sn 4589

This theorem is used by:  fnsnsplit  7220  fsnunf2  7222  difsnexi  7807  difsnen  9116  enfixsn  9143  pssnn  9222  dif1ennnALT  9306  frfi  9314  dif1card  10128  hashgt23el  14610  hashfun  14623  fprodfvdvdsd  16548  prmdvdsprmo  17264  mreexexlem4d  17871  symgextf1  19686  symgextfo  19687  symgfixf1  19702  gsumdifsnd  20226  gsummgp0  20598  islindf4  22199  lindsenlbs  22212  scmatf1  22901  gsummatr01  23029  tdeglem4  26433  finsumvtxdg2sstep  30187  dfconngr1  30846  fmptunsnop  33390  satfv1lem  36335  bj-raldifsn  38291  lindsadd  38804  poimirlem25  38831  poimirlem27  38833  hdmap14lem4a  43194  hdmap14lem13  43203  supxrmnf2  46716  infxrpnf2  46746  fsumnncl  46857  hoidmv1lelem2  47875  gsumdifsndf  49551  mgpsumunsn  49804