Theorem difsnid 4743

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 4087	. 2 ⊢ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = ({𝐵} ∪ (𝐴 ∖ {𝐵}))
2		snssi 4741	. . 3 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴)
3		undif 4415	. . 3 ⊢ ({𝐵} ⊆ 𝐴 ↔ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
4	2, 3	sylib 217	. 2 ⊢ (𝐵 ∈ 𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
5	1, 4	eqtrid 2790	1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106   ∖ cdif 3884   ∪ cun 3885   ⊆ wss 3887  {csn 4561

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-sn 4562

This theorem is referenced by:  fnsnsplit  7056  fsnunf2  7058  difsnexi  7611  difsnen  8840  enfixsn  8868  pssnn  8951  phplem2OLD  9001  pssnnOLD  9040  dif1enALT  9050  frfi  9059  xpfi  9085  dif1card  9766  hashgt23el  14139  hashfun  14152  fprodfvdvdsd  16043  prmdvdsprmo  16743  mreexexlem4d  17356  symgextf1  19029  symgextfo  19030  symgfixf1  19045  gsumdifsnd  19562  gsummgp0  19847  islindf4  21045  scmatf1  21680  gsummatr01  21808  tdeglem4  25224  tdeglem4OLD  25225  finsumvtxdg2sstep  27916  dfconngr1  28552  satfv1lem  33324  bj-raldifsn  35271  lindsadd  35770  lindsenlbs  35772  poimirlem25  35802  poimirlem27  35804  hdmap14lem4a  39885  hdmap14lem13  39894  supxrmnf2  42973  infxrpnf2  43003  fsumnncl  43113  hoidmv1lelem2  44130  gsumdifsndf  45375  mgpsumunsn  45697