Theorem difsnid 4282

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 3719	. 2 ⊢ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = ({𝐵} ∪ (𝐴 ∖ {𝐵}))
2		snssi 4280	. . 3 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴)
3		undif 4001	. . 3 ⊢ ({𝐵} ⊆ 𝐴 ↔ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
4	2, 3	sylib 207	. 2 ⊢ (𝐵 ∈ 𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
5	1, 4	syl5eq 2656	1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977   ∖ cdif 3537   ∪ cun 3538   ⊆ wss 3540  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-sn 4126

This theorem is referenced by:  fnsnsplit  6355  fsnunf2  6357  difsnexi  6864  difsnen  7927  enfixsn  7954  phplem2  8025  pssnn  8063  dif1en  8078  frfi  8090  xpfi  8116  dif1card  8716  hashfun  13084  fprodfvdvdsd  14896  prmdvdsprmo  15584  mreexexlem4d  16130  symgextf1  17664  symgextfo  17665  symgfixf1  17680  gsumdifsnd  18183  gsummgp0  18431  islindf4  19996  scmatf1  20156  gsummatr01  20284  tdeglem4  23624  dfconngra1  26199  lindsenlbs  32574  poimirlem25  32604  poimirlem27  32606  hdmap14lem4a  36181  hdmap14lem13  36190  fsumnncl  38638  hoidmv1lelem2  39482  dfconngr1  41355  mgpsumunsn  41933  gsumdifsndf  41937