Theorem difsnid 4809

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ∖ cdif 3947   ∪ cun 3948   ⊆ wss 3950  {csn 4625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-sn 4626

This theorem is referenced by:  fnsnsplit  7205  fsnunf2  7207  difsnexi  7782  difsnen  9094  enfixsn  9122  pssnn  9209  phplem2OLD  9256  dif1ennnALT  9312  frfi  9322  xpfiOLD  9360  dif1card  10051  hashgt23el  14464  hashfun  14477  fprodfvdvdsd  16372  prmdvdsprmo  17081  mreexexlem4d  17691  symgextf1  19440  symgextfo  19441  symgfixf1  19456  gsumdifsnd  19980  gsummgp0  20316  islindf4  21859  scmatf1  22538  gsummatr01  22666  tdeglem4  26100  finsumvtxdg2sstep  29568  dfconngr1  30208  fmptunsnop  32710  satfv1lem  35368  bj-raldifsn  37102  lindsadd  37621  lindsenlbs  37623  poimirlem25  37653  poimirlem27  37655  hdmap14lem4a  41874  hdmap14lem13  41883  supxrmnf2  45449  infxrpnf2  45479  fsumnncl  45592  hoidmv1lelem2  46612  gsumdifsndf  48102  mgpsumunsn  48282