Theorem difsnid 4814

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   ∖ cdif 3946   ∪ cun 3947   ⊆ wss 3949  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-sn 4630

This theorem is referenced by:  fnsnsplit  7182  fsnunf2  7184  difsnexi  7748  difsnen  9053  enfixsn  9081  pssnn  9168  phplem2OLD  9218  pssnnOLD  9265  dif1ennnALT  9277  frfi  9288  xpfiOLD  9318  dif1card  10005  hashgt23el  14384  hashfun  14397  fprodfvdvdsd  16277  prmdvdsprmo  16975  mreexexlem4d  17591  symgextf1  19289  symgextfo  19290  symgfixf1  19305  gsumdifsnd  19829  gsummgp0  20130  islindf4  21393  scmatf1  22033  gsummatr01  22161  tdeglem4  25577  tdeglem4OLD  25578  finsumvtxdg2sstep  28806  dfconngr1  29441  satfv1lem  34353  bj-raldifsn  35981  lindsadd  36481  lindsenlbs  36483  poimirlem25  36513  poimirlem27  36515  hdmap14lem4a  40742  hdmap14lem13  40751  supxrmnf2  44143  infxrpnf2  44173  fsumnncl  44288  hoidmv1lelem2  45308  gsumdifsndf  46591  mgpsumunsn  47037