Theorem difsnid 4740

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559

This theorem is referenced by:  fnsnsplit  7038  fsnunf2  7040  difsnexi  7589  difsnen  8794  enfixsn  8821  phplem2  8893  pssnn  8913  pssnnOLD  8969  dif1enALT  8980  frfi  8989  xpfi  9015  dif1card  9697  hashgt23el  14067  hashfun  14080  fprodfvdvdsd  15971  prmdvdsprmo  16671  mreexexlem4d  17273  symgextf1  18944  symgextfo  18945  symgfixf1  18960  gsumdifsnd  19477  gsummgp0  19762  islindf4  20955  scmatf1  21588  gsummatr01  21716  tdeglem4  25129  tdeglem4OLD  25130  finsumvtxdg2sstep  27819  dfconngr1  28453  satfv1lem  33224  bj-raldifsn  35198  lindsadd  35697  lindsenlbs  35699  poimirlem25  35729  poimirlem27  35731  hdmap14lem4a  39812  hdmap14lem13  39821  supxrmnf2  42863  infxrpnf2  42893  fsumnncl  43003  hoidmv1lelem2  44020  gsumdifsndf  45263  mgpsumunsn  45585