Theorem difsnid 4806

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		uncom 4149	. 2 ⊢ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = ({𝐵} ∪ (𝐴 ∖ {𝐵}))
2		snssi 4804	. . 3 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴)
3		undif 4477	. . 3 ⊢ ({𝐵} ⊆ 𝐴 ↔ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
4	2, 3	sylib 217	. 2 ⊢ (𝐵 ∈ 𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
5	1, 4	eqtrid 2783	1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ∖ cdif 3941   ∪ cun 3942   ⊆ wss 3944  {csn 4622

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-sn 4623

This theorem is referenced by:  fnsnsplit  7166  fsnunf2  7168  difsnexi  7731  difsnen  9036  enfixsn  9064  pssnn  9151  phplem2OLD  9201  pssnnOLD  9248  dif1ennnALT  9260  frfi  9271  xpfiOLD  9301  dif1card  9987  hashgt23el  14366  hashfun  14379  fprodfvdvdsd  16259  prmdvdsprmo  16957  mreexexlem4d  17573  symgextf1  19253  symgextfo  19254  symgfixf1  19269  gsumdifsnd  19788  gsummgp0  20085  islindf4  21326  scmatf1  21962  gsummatr01  22090  tdeglem4  25506  tdeglem4OLD  25507  finsumvtxdg2sstep  28671  dfconngr1  29306  satfv1lem  34182  bj-raldifsn  35783  lindsadd  36283  lindsenlbs  36285  poimirlem25  36315  poimirlem27  36317  hdmap14lem4a  40545  hdmap14lem13  40554  supxrmnf2  43914  infxrpnf2  43944  fsumnncl  44059  hoidmv1lelem2  45079  gsumdifsndf  46361  mgpsumunsn  46683