Theorem difsnid 4766

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ∖ cdif 3898   ∪ cun 3899   ⊆ wss 3901  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-sn 4581

This theorem is referenced by:  fnsnsplit  7130  fsnunf2  7132  difsnexi  7706  difsnen  8987  enfixsn  9014  pssnn  9093  dif1ennnALT  9177  frfi  9185  dif1card  9920  hashgt23el  14347  hashfun  14360  fprodfvdvdsd  16261  prmdvdsprmo  16970  mreexexlem4d  17570  symgextf1  19350  symgextfo  19351  symgfixf1  19366  gsumdifsnd  19890  gsummgp0  20253  islindf4  21793  scmatf1  22475  gsummatr01  22603  tdeglem4  26021  finsumvtxdg2sstep  29623  dfconngr1  30263  fmptunsnop  32779  satfv1lem  35556  bj-raldifsn  37305  lindsadd  37814  lindsenlbs  37816  poimirlem25  37846  poimirlem27  37848  hdmap14lem4a  42131  hdmap14lem13  42140  supxrmnf2  45677  infxrpnf2  45707  fsumnncl  45818  hoidmv1lelem2  46836  gsumdifsndf  48427  mgpsumunsn  48607