Theorem difsnid 4835

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   ∖ cdif 3973   ∪ cun 3974   ⊆ wss 3976  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-sn 4649

This theorem is referenced by:  fnsnsplit  7218  fsnunf2  7220  difsnexi  7796  difsnen  9119  enfixsn  9147  pssnn  9234  phplem2OLD  9281  dif1ennnALT  9339  frfi  9349  xpfiOLD  9387  dif1card  10079  hashgt23el  14473  hashfun  14486  fprodfvdvdsd  16382  prmdvdsprmo  17089  mreexexlem4d  17705  symgextf1  19463  symgextfo  19464  symgfixf1  19479  gsumdifsnd  20003  gsummgp0  20341  islindf4  21881  scmatf1  22558  gsummatr01  22686  tdeglem4  26119  finsumvtxdg2sstep  29585  dfconngr1  30220  satfv1lem  35330  bj-raldifsn  37066  lindsadd  37573  lindsenlbs  37575  poimirlem25  37605  poimirlem27  37607  hdmap14lem4a  41828  hdmap14lem13  41837  supxrmnf2  45348  infxrpnf2  45378  fsumnncl  45493  hoidmv1lelem2  46513  gsumdifsndf  47904  mgpsumunsn  48086