Theorem difsnid 4723

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 4067	. 2 ⊢ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = ({𝐵} ∪ (𝐴 ∖ {𝐵}))
2		snssi 4721	. . 3 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴)
3		undif 4396	. . 3 ⊢ ({𝐵} ⊆ 𝐴 ↔ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
4	2, 3	sylib 221	. 2 ⊢ (𝐵 ∈ 𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
5	1, 4	eqtrid 2789	1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2110   ∖ cdif 3863   ∪ cun 3864   ⊆ wss 3866  {csn 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-sn 4542

This theorem is referenced by:  fnsnsplit  6999  fsnunf2  7001  difsnexi  7546  difsnen  8727  enfixsn  8754  phplem2  8826  pssnn  8846  pssnnOLD  8895  dif1enALT  8907  frfi  8916  xpfi  8942  dif1card  9624  hashgt23el  13991  hashfun  14004  fprodfvdvdsd  15895  prmdvdsprmo  16595  mreexexlem4d  17150  symgextf1  18813  symgextfo  18814  symgfixf1  18829  gsumdifsnd  19346  gsummgp0  19626  islindf4  20800  scmatf1  21428  gsummatr01  21556  tdeglem4  24957  tdeglem4OLD  24958  finsumvtxdg2sstep  27637  dfconngr1  28271  satfv1lem  33037  bj-raldifsn  35006  lindsadd  35507  lindsenlbs  35509  poimirlem25  35539  poimirlem27  35541  hdmap14lem4a  39622  hdmap14lem13  39631  supxrmnf2  42646  infxrpnf2  42678  fsumnncl  42788  hoidmv1lelem2  43805  gsumdifsndf  45048  mgpsumunsn  45370