Theorem difsnid 4753

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∖ cdif 3886   ∪ cun 3887   ⊆ wss 3889  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-sn 4568

This theorem is referenced by:  fnsnsplit  7139  fsnunf2  7141  difsnexi  7715  difsnen  8997  enfixsn  9024  pssnn  9103  dif1ennnALT  9187  frfi  9195  dif1card  9932  hashgt23el  14386  hashfun  14399  fprodfvdvdsd  16303  prmdvdsprmo  17013  mreexexlem4d  17613  symgextf1  19396  symgextfo  19397  symgfixf1  19412  gsumdifsnd  19936  gsummgp0  20297  islindf4  21818  scmatf1  22496  gsummatr01  22624  tdeglem4  26025  finsumvtxdg2sstep  29618  dfconngr1  30258  fmptunsnop  32773  satfv1lem  35544  bj-raldifsn  37412  lindsadd  37934  lindsenlbs  37936  poimirlem25  37966  poimirlem27  37968  hdmap14lem4a  42317  hdmap14lem13  42326  supxrmnf2  45861  infxrpnf2  45891  fsumnncl  46002  hoidmv1lelem2  47020  gsumdifsndf  48657  mgpsumunsn  48837