Theorem difsnid 4737

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 4129	. 2 ⊢ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = ({𝐵} ∪ (𝐴 ∖ {𝐵}))
2		snssi 4735	. . 3 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴)
3		undif 4430	. . 3 ⊢ ({𝐵} ⊆ 𝐴 ↔ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
4	2, 3	sylib 220	. 2 ⊢ (𝐵 ∈ 𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
5	1, 4	syl5eq 2868	1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110   ∖ cdif 3933   ∪ cun 3934   ⊆ wss 3936  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-sn 4562

This theorem is referenced by:  fnsnsplit  6941  fsnunf2  6943  difsnexi  7477  difsnen  8593  enfixsn  8620  phplem2  8691  pssnn  8730  dif1en  8745  frfi  8757  xpfi  8783  dif1card  9430  hashgt23el  13779  hashfun  13792  fprodfvdvdsd  15677  prmdvdsprmo  16372  mreexexlem4d  16912  symgextf1  18543  symgextfo  18544  symgfixf1  18559  gsumdifsnd  19075  gsummgp0  19352  islindf4  20976  scmatf1  21134  gsummatr01  21262  tdeglem4  24648  finsumvtxdg2sstep  27325  dfconngr1  27961  satfv1lem  32604  bj-raldifsn  34386  lindsadd  34879  lindsenlbs  34881  poimirlem25  34911  poimirlem27  34913  hdmap14lem4a  39001  hdmap14lem13  39010  supxrmnf2  41699  infxrpnf2  41731  fsumnncl  41844  hoidmv1lelem2  42867  gsumdifsndf  44081  mgpsumunsn  44402