Theorem difsnid 4741

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-sn 4556

This theorem is referenced by:  fnsnsplit  7128  fsnunf2  7130  difsnexi  7704  difsnen  8987  enfixsn  9014  pssnn  9093  dif1ennnALT  9177  frfi  9185  dif1card  9923  hashgt23el  14377  hashfun  14390  fprodfvdvdsd  16294  prmdvdsprmo  17004  mreexexlem4d  17604  symgextf1  19387  symgextfo  19388  symgfixf1  19403  gsumdifsnd  19927  gsummgp0  20288  islindf4  21813  scmatf1  22514  gsummatr01  22642  tdeglem4  26043  finsumvtxdg2sstep  29636  dfconngr1  30276  fmptunsnop  32792  satfv1lem  35590  bj-raldifsn  37458  lindsadd  37980  lindsenlbs  37982  poimirlem25  38012  poimirlem27  38014  hdmap14lem4a  42363  hdmap14lem13  42372  supxrmnf2  45876  infxrpnf2  45906  fsumnncl  46017  hoidmv1lelem2  47035  gsumdifsndf  48672  mgpsumunsn  48852